(0) Obligation:
Clauses:
occur(X, [], 0).
occur(X, .(Y, Z), W) :- ->(','(count(X, Y, A), occur(X, Z, B)), is(W, +(A, B))).
count(X, [], 0).
count(X, .(Y, Z), W) :- ->(count(X, Z, W1), addx(X, Y, W1, W)).
addx(X, X, W1, W) :- is(W, +(W1, 1)).
addx(X, Y, W1, W1) :- =\=(X, Y).
occurall([], X, []).
occurall(.(X, Y), Z, .(.(X, .(W, [])), V)) :- ','(occur(X, Z, W), occurall(Y, Z, V)).
get_query(X, Y) :- ','(=(X, .(5, .(3, .(6, .(7, .(2, .(1, .(4, .(11, .(8, [])))))))))), =(Y, .(.(3, .(4, .(5, .(6, .(7, .(6, .(5, .(4, .(5, .(6, .(5, .(4, .(3, .(5, .(6, .(2, .(3, .(4, .(5, []))))))))))))))))))), .(.(3, .(4, [])), .(.(4, .(5, .(5, .(5, .(5, []))))), .(.(13, .(4, .(5, .(6, .(7, .(8, .(7, .(6, .(5, .(4, .(5, .(6, .(7, .(6, .(5, .(5, .(5, .(5, .(4, .(5, .(5, .(5, .(6, .(6, .(6, .(5, .(5, .(4, [])))))))))))))))))))))))))))), .(.(1, .(2, .(2, .(2, .(1, .(1, .(3, .(2, .(3, .(2, .(3, .(3, .(3, []))))))))))))), .(.(3, .(4, [])), .(.(4, .(5, .(5, .(5, .(5, []))))), .(.(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(7, .(6, .(5, .(4, .(5, .(6, .(7, .(6, .(5, .(5, .(5, .(5, .(4, .(5, .(5, .(5, .(6, .(6, .(6, .(5, [])))))))))))))))))))))))))))), .(.(1, .(2, .(2, .(2, .(1, .(1, .(3, .(2, .(3, .(2, .(3, .(3, .(3, []))))))))))))), .(.(3, .(4, [])), .(.(4, .(5, .(5, .(5, .(5, []))))), .(.(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(7, .(6, .(5, .(4, .(5, .(6, .(7, .(6, .(5, []))))))))))))))))), .(.(5, .(5, .(5, .(4, .(5, .(5, .(5, .(6, .(6, .(6, .(5, .(5, .(4, []))))))))))))), .(.(1, .(2, .(2, .(2, .(1, .(1, .(3, .(2, .(3, .(2, .(3, .(3, .(3, []))))))))))))), .([], .(.(3, .(4, [])), .(.(4, .(5, .(5, .(5, .(5, []))))), .(.(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(7, .(6, .(5, .(4, .(5, .(6, .(7, .(6, .(5, []))))))))))))))))), .(.(5, .(5, .(5, .(4, .(5, .(5, .(5, .(6, .(6, .(6, .(5, .(5, .(4, []))))))))))))), .(.(1, .(2, .(2, .(2, .(1, .(1, .(3, .(2, .(3, .(2, .(3, .(3, .(3, []))))))))))))), .(.(3, .(4, [])), .(.(4, .(5, .(5, .(5, .(5, []))))), .(.(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(7, .(6, .(5, .(4, .(5, .(6, .(7, .(6, .(5, []))))))))))))))))), .(.(5, .(5, .(5, .(4, .(5, .(5, .(5, .(6, .(6, .(6, .(5, .(5, .(4, []))))))))))))), .(.(1, .(2, .(2, .(2, .(1, .(1, .(3, .(2, .(3, .(2, .(3, .(3, .(3, []))))))))))))), .(.(5, []), .(.(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, []))))))))))))))))))))))))), []))))))))))))))))))))))))))))).
Query: occurall(g,g,a)
(1) IfThenElseTransformerProof (EQUIVALENT transformation)
Transformed all if-then-else-constructs [PROLOG].
(2) Obligation:
Clauses:
occur(X, [], 0).
occur(X, .(Y, Z), W) :- if(X, Y, A, Z, B, W).
count(X, [], 0).
count(X, .(Y, Z), W) :- if1(X, Z, W1, Y, W).
addx(X, X, W1, W) :- is(W, +(W1, 1)).
addx(X, Y, W1, W1) :- =\=(X, Y).
occurall([], X, []).
occurall(.(X, Y), Z, .(.(X, .(W, [])), V)) :- ','(occur(X, Z, W), occurall(Y, Z, V)).
get_query(X, Y) :- ','(=(X, .(5, .(3, .(6, .(7, .(2, .(1, .(4, .(11, .(8, [])))))))))), =(Y, .(.(3, .(4, .(5, .(6, .(7, .(6, .(5, .(4, .(5, .(6, .(5, .(4, .(3, .(5, .(6, .(2, .(3, .(4, .(5, []))))))))))))))))))), .(.(3, .(4, [])), .(.(4, .(5, .(5, .(5, .(5, []))))), .(.(13, .(4, .(5, .(6, .(7, .(8, .(7, .(6, .(5, .(4, .(5, .(6, .(7, .(6, .(5, .(5, .(5, .(5, .(4, .(5, .(5, .(5, .(6, .(6, .(6, .(5, .(5, .(4, [])))))))))))))))))))))))))))), .(.(1, .(2, .(2, .(2, .(1, .(1, .(3, .(2, .(3, .(2, .(3, .(3, .(3, []))))))))))))), .(.(3, .(4, [])), .(.(4, .(5, .(5, .(5, .(5, []))))), .(.(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(7, .(6, .(5, .(4, .(5, .(6, .(7, .(6, .(5, .(5, .(5, .(5, .(4, .(5, .(5, .(5, .(6, .(6, .(6, .(5, [])))))))))))))))))))))))))))), .(.(1, .(2, .(2, .(2, .(1, .(1, .(3, .(2, .(3, .(2, .(3, .(3, .(3, []))))))))))))), .(.(3, .(4, [])), .(.(4, .(5, .(5, .(5, .(5, []))))), .(.(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(7, .(6, .(5, .(4, .(5, .(6, .(7, .(6, .(5, []))))))))))))))))), .(.(5, .(5, .(5, .(4, .(5, .(5, .(5, .(6, .(6, .(6, .(5, .(5, .(4, []))))))))))))), .(.(1, .(2, .(2, .(2, .(1, .(1, .(3, .(2, .(3, .(2, .(3, .(3, .(3, []))))))))))))), .([], .(.(3, .(4, [])), .(.(4, .(5, .(5, .(5, .(5, []))))), .(.(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(7, .(6, .(5, .(4, .(5, .(6, .(7, .(6, .(5, []))))))))))))))))), .(.(5, .(5, .(5, .(4, .(5, .(5, .(5, .(6, .(6, .(6, .(5, .(5, .(4, []))))))))))))), .(.(1, .(2, .(2, .(2, .(1, .(1, .(3, .(2, .(3, .(2, .(3, .(3, .(3, []))))))))))))), .(.(3, .(4, [])), .(.(4, .(5, .(5, .(5, .(5, []))))), .(.(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(7, .(6, .(5, .(4, .(5, .(6, .(7, .(6, .(5, []))))))))))))))))), .(.(5, .(5, .(5, .(4, .(5, .(5, .(5, .(6, .(6, .(6, .(5, .(5, .(4, []))))))))))))), .(.(1, .(2, .(2, .(2, .(1, .(1, .(3, .(2, .(3, .(2, .(3, .(3, .(3, []))))))))))))), .(.(5, []), .(.(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, []))))))))))))))))))))))))), []))))))))))))))))))))))))))))).
if(X, Y, A, Z, B, W) :- ','(call(','(count(X, Y, A), occur(X, Z, B))), ','(!, is(W, +(A, B)))).
if1(X, Z, W1, Y, W) :- ','(call(count(X, Z, W1)), ','(!, addx(X, Y, W1, W))).
Query: occurall(g,g,a)
(3) CallTransformerProof (EQUIVALENT transformation)
Transformed all call-constructs [PROLOG].
(4) Obligation:
Clauses:
occur(X, [], 0).
occur(X, .(Y, Z), W) :- if(X, Y, A, Z, B, W).
count(X, [], 0).
count(X, .(Y, Z), W) :- if1(X, Z, W1, Y, W).
addx(X, X, W1, W) :- is(W, +(W1, 1)).
addx(X, Y, W1, W1) :- =\=(X, Y).
occurall([], X, []).
occurall(.(X, Y), Z, .(.(X, .(W, [])), V)) :- ','(occur(X, Z, W), occurall(Y, Z, V)).
get_query(X, Y) :- ','(=(X, .(5, .(3, .(6, .(7, .(2, .(1, .(4, .(11, .(8, [])))))))))), =(Y, .(.(3, .(4, .(5, .(6, .(7, .(6, .(5, .(4, .(5, .(6, .(5, .(4, .(3, .(5, .(6, .(2, .(3, .(4, .(5, []))))))))))))))))))), .(.(3, .(4, [])), .(.(4, .(5, .(5, .(5, .(5, []))))), .(.(13, .(4, .(5, .(6, .(7, .(8, .(7, .(6, .(5, .(4, .(5, .(6, .(7, .(6, .(5, .(5, .(5, .(5, .(4, .(5, .(5, .(5, .(6, .(6, .(6, .(5, .(5, .(4, [])))))))))))))))))))))))))))), .(.(1, .(2, .(2, .(2, .(1, .(1, .(3, .(2, .(3, .(2, .(3, .(3, .(3, []))))))))))))), .(.(3, .(4, [])), .(.(4, .(5, .(5, .(5, .(5, []))))), .(.(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(7, .(6, .(5, .(4, .(5, .(6, .(7, .(6, .(5, .(5, .(5, .(5, .(4, .(5, .(5, .(5, .(6, .(6, .(6, .(5, [])))))))))))))))))))))))))))), .(.(1, .(2, .(2, .(2, .(1, .(1, .(3, .(2, .(3, .(2, .(3, .(3, .(3, []))))))))))))), .(.(3, .(4, [])), .(.(4, .(5, .(5, .(5, .(5, []))))), .(.(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(7, .(6, .(5, .(4, .(5, .(6, .(7, .(6, .(5, []))))))))))))))))), .(.(5, .(5, .(5, .(4, .(5, .(5, .(5, .(6, .(6, .(6, .(5, .(5, .(4, []))))))))))))), .(.(1, .(2, .(2, .(2, .(1, .(1, .(3, .(2, .(3, .(2, .(3, .(3, .(3, []))))))))))))), .([], .(.(3, .(4, [])), .(.(4, .(5, .(5, .(5, .(5, []))))), .(.(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(7, .(6, .(5, .(4, .(5, .(6, .(7, .(6, .(5, []))))))))))))))))), .(.(5, .(5, .(5, .(4, .(5, .(5, .(5, .(6, .(6, .(6, .(5, .(5, .(4, []))))))))))))), .(.(1, .(2, .(2, .(2, .(1, .(1, .(3, .(2, .(3, .(2, .(3, .(3, .(3, []))))))))))))), .(.(3, .(4, [])), .(.(4, .(5, .(5, .(5, .(5, []))))), .(.(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(7, .(6, .(5, .(4, .(5, .(6, .(7, .(6, .(5, []))))))))))))))))), .(.(5, .(5, .(5, .(4, .(5, .(5, .(5, .(6, .(6, .(6, .(5, .(5, .(4, []))))))))))))), .(.(1, .(2, .(2, .(2, .(1, .(1, .(3, .(2, .(3, .(2, .(3, .(3, .(3, []))))))))))))), .(.(5, []), .(.(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, []))))))))))))))))))))))))), []))))))))))))))))))))))))))))).
if(X, Y, A, Z, B, W) :- ','(call1(X, Y, A, Z, B), ','(!, is(W, +(A, B)))).
if1(X, Z, W1, Y, W) :- ','(call2(X, Z, W1), ','(!, addx(X, Y, W1, W))).
call1(X, Y, A, Z, B) :- ','(count(X, Y, A), occur(X, Z, B)).
call2(X, Z, W1) :- count(X, Z, W1).
Query: occurall(g,g,a)
(5) CutEliminatorProof (SOUND transformation)
Eliminated all cuts by simply ignoring them[PROLOG].
(6) Obligation:
Clauses:
occur(X, [], 0).
occur(X, .(Y, Z), W) :- if(X, Y, A, Z, B, W).
count(X, [], 0).
count(X, .(Y, Z), W) :- if1(X, Z, W1, Y, W).
addx(X, X, W1, W) :- is(W, +(W1, 1)).
addx(X, Y, W1, W1) :- =\=(X, Y).
occurall([], X, []).
occurall(.(X, Y), Z, .(.(X, .(W, [])), V)) :- ','(occur(X, Z, W), occurall(Y, Z, V)).
get_query(X, Y) :- ','(=(X, .(5, .(3, .(6, .(7, .(2, .(1, .(4, .(11, .(8, [])))))))))), =(Y, .(.(3, .(4, .(5, .(6, .(7, .(6, .(5, .(4, .(5, .(6, .(5, .(4, .(3, .(5, .(6, .(2, .(3, .(4, .(5, []))))))))))))))))))), .(.(3, .(4, [])), .(.(4, .(5, .(5, .(5, .(5, []))))), .(.(13, .(4, .(5, .(6, .(7, .(8, .(7, .(6, .(5, .(4, .(5, .(6, .(7, .(6, .(5, .(5, .(5, .(5, .(4, .(5, .(5, .(5, .(6, .(6, .(6, .(5, .(5, .(4, [])))))))))))))))))))))))))))), .(.(1, .(2, .(2, .(2, .(1, .(1, .(3, .(2, .(3, .(2, .(3, .(3, .(3, []))))))))))))), .(.(3, .(4, [])), .(.(4, .(5, .(5, .(5, .(5, []))))), .(.(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(7, .(6, .(5, .(4, .(5, .(6, .(7, .(6, .(5, .(5, .(5, .(5, .(4, .(5, .(5, .(5, .(6, .(6, .(6, .(5, [])))))))))))))))))))))))))))), .(.(1, .(2, .(2, .(2, .(1, .(1, .(3, .(2, .(3, .(2, .(3, .(3, .(3, []))))))))))))), .(.(3, .(4, [])), .(.(4, .(5, .(5, .(5, .(5, []))))), .(.(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(7, .(6, .(5, .(4, .(5, .(6, .(7, .(6, .(5, []))))))))))))))))), .(.(5, .(5, .(5, .(4, .(5, .(5, .(5, .(6, .(6, .(6, .(5, .(5, .(4, []))))))))))))), .(.(1, .(2, .(2, .(2, .(1, .(1, .(3, .(2, .(3, .(2, .(3, .(3, .(3, []))))))))))))), .([], .(.(3, .(4, [])), .(.(4, .(5, .(5, .(5, .(5, []))))), .(.(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(7, .(6, .(5, .(4, .(5, .(6, .(7, .(6, .(5, []))))))))))))))))), .(.(5, .(5, .(5, .(4, .(5, .(5, .(5, .(6, .(6, .(6, .(5, .(5, .(4, []))))))))))))), .(.(1, .(2, .(2, .(2, .(1, .(1, .(3, .(2, .(3, .(2, .(3, .(3, .(3, []))))))))))))), .(.(3, .(4, [])), .(.(4, .(5, .(5, .(5, .(5, []))))), .(.(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(7, .(6, .(5, .(4, .(5, .(6, .(7, .(6, .(5, []))))))))))))))))), .(.(5, .(5, .(5, .(4, .(5, .(5, .(5, .(6, .(6, .(6, .(5, .(5, .(4, []))))))))))))), .(.(1, .(2, .(2, .(2, .(1, .(1, .(3, .(2, .(3, .(2, .(3, .(3, .(3, []))))))))))))), .(.(5, []), .(.(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, []))))))))))))))))))))))))), []))))))))))))))))))))))))))))).
if(X, Y, A, Z, B, W) :- ','(call1(X, Y, A, Z, B), is(W, +(A, B))).
if1(X, Z, W1, Y, W) :- ','(call2(X, Z, W1), addx(X, Y, W1, W)).
call1(X, Y, A, Z, B) :- ','(count(X, Y, A), occur(X, Z, B)).
call2(X, Z, W1) :- count(X, Z, W1).
Query: occurall(g,g,a)
(7) UnifyTransformerProof (EQUIVALENT transformation)
Added a fact for the built-in = predicate [PROLOG].
(8) Obligation:
Clauses:
occur(X, [], 0).
occur(X, .(Y, Z), W) :- if(X, Y, A, Z, B, W).
count(X, [], 0).
count(X, .(Y, Z), W) :- if1(X, Z, W1, Y, W).
addx(X, X, W1, W) :- is(W, +(W1, 1)).
addx(X, Y, W1, W1) :- =\=(X, Y).
occurall([], X, []).
occurall(.(X, Y), Z, .(.(X, .(W, [])), V)) :- ','(occur(X, Z, W), occurall(Y, Z, V)).
get_query(X, Y) :- ','(=(X, .(5, .(3, .(6, .(7, .(2, .(1, .(4, .(11, .(8, [])))))))))), =(Y, .(.(3, .(4, .(5, .(6, .(7, .(6, .(5, .(4, .(5, .(6, .(5, .(4, .(3, .(5, .(6, .(2, .(3, .(4, .(5, []))))))))))))))))))), .(.(3, .(4, [])), .(.(4, .(5, .(5, .(5, .(5, []))))), .(.(13, .(4, .(5, .(6, .(7, .(8, .(7, .(6, .(5, .(4, .(5, .(6, .(7, .(6, .(5, .(5, .(5, .(5, .(4, .(5, .(5, .(5, .(6, .(6, .(6, .(5, .(5, .(4, [])))))))))))))))))))))))))))), .(.(1, .(2, .(2, .(2, .(1, .(1, .(3, .(2, .(3, .(2, .(3, .(3, .(3, []))))))))))))), .(.(3, .(4, [])), .(.(4, .(5, .(5, .(5, .(5, []))))), .(.(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(7, .(6, .(5, .(4, .(5, .(6, .(7, .(6, .(5, .(5, .(5, .(5, .(4, .(5, .(5, .(5, .(6, .(6, .(6, .(5, [])))))))))))))))))))))))))))), .(.(1, .(2, .(2, .(2, .(1, .(1, .(3, .(2, .(3, .(2, .(3, .(3, .(3, []))))))))))))), .(.(3, .(4, [])), .(.(4, .(5, .(5, .(5, .(5, []))))), .(.(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(7, .(6, .(5, .(4, .(5, .(6, .(7, .(6, .(5, []))))))))))))))))), .(.(5, .(5, .(5, .(4, .(5, .(5, .(5, .(6, .(6, .(6, .(5, .(5, .(4, []))))))))))))), .(.(1, .(2, .(2, .(2, .(1, .(1, .(3, .(2, .(3, .(2, .(3, .(3, .(3, []))))))))))))), .([], .(.(3, .(4, [])), .(.(4, .(5, .(5, .(5, .(5, []))))), .(.(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(7, .(6, .(5, .(4, .(5, .(6, .(7, .(6, .(5, []))))))))))))))))), .(.(5, .(5, .(5, .(4, .(5, .(5, .(5, .(6, .(6, .(6, .(5, .(5, .(4, []))))))))))))), .(.(1, .(2, .(2, .(2, .(1, .(1, .(3, .(2, .(3, .(2, .(3, .(3, .(3, []))))))))))))), .(.(3, .(4, [])), .(.(4, .(5, .(5, .(5, .(5, []))))), .(.(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(7, .(6, .(5, .(4, .(5, .(6, .(7, .(6, .(5, []))))))))))))))))), .(.(5, .(5, .(5, .(4, .(5, .(5, .(5, .(6, .(6, .(6, .(5, .(5, .(4, []))))))))))))), .(.(1, .(2, .(2, .(2, .(1, .(1, .(3, .(2, .(3, .(2, .(3, .(3, .(3, []))))))))))))), .(.(5, []), .(.(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, []))))))))))))))))))))))))), []))))))))))))))))))))))))))))).
if(X, Y, A, Z, B, W) :- ','(call1(X, Y, A, Z, B), is(W, +(A, B))).
if1(X, Z, W1, Y, W) :- ','(call2(X, Z, W1), addx(X, Y, W1, W)).
call1(X, Y, A, Z, B) :- ','(count(X, Y, A), occur(X, Z, B)).
call2(X, Z, W1) :- count(X, Z, W1).
=(X, X).
Query: occurall(g,g,a)
(9) UndefinedPredicateHandlerProof (SOUND transformation)
Added facts for all undefined predicates [PROLOG].
(10) Obligation:
Clauses:
occur(X, [], 0).
occur(X, .(Y, Z), W) :- if(X, Y, A, Z, B, W).
count(X, [], 0).
count(X, .(Y, Z), W) :- if1(X, Z, W1, Y, W).
addx(X, X, W1, W) :- is(W, +(W1, 1)).
addx(X, Y, W1, W1) :- =\=(X, Y).
occurall([], X, []).
occurall(.(X, Y), Z, .(.(X, .(W, [])), V)) :- ','(occur(X, Z, W), occurall(Y, Z, V)).
get_query(X, Y) :- ','(=(X, .(5, .(3, .(6, .(7, .(2, .(1, .(4, .(11, .(8, [])))))))))), =(Y, .(.(3, .(4, .(5, .(6, .(7, .(6, .(5, .(4, .(5, .(6, .(5, .(4, .(3, .(5, .(6, .(2, .(3, .(4, .(5, []))))))))))))))))))), .(.(3, .(4, [])), .(.(4, .(5, .(5, .(5, .(5, []))))), .(.(13, .(4, .(5, .(6, .(7, .(8, .(7, .(6, .(5, .(4, .(5, .(6, .(7, .(6, .(5, .(5, .(5, .(5, .(4, .(5, .(5, .(5, .(6, .(6, .(6, .(5, .(5, .(4, [])))))))))))))))))))))))))))), .(.(1, .(2, .(2, .(2, .(1, .(1, .(3, .(2, .(3, .(2, .(3, .(3, .(3, []))))))))))))), .(.(3, .(4, [])), .(.(4, .(5, .(5, .(5, .(5, []))))), .(.(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(7, .(6, .(5, .(4, .(5, .(6, .(7, .(6, .(5, .(5, .(5, .(5, .(4, .(5, .(5, .(5, .(6, .(6, .(6, .(5, [])))))))))))))))))))))))))))), .(.(1, .(2, .(2, .(2, .(1, .(1, .(3, .(2, .(3, .(2, .(3, .(3, .(3, []))))))))))))), .(.(3, .(4, [])), .(.(4, .(5, .(5, .(5, .(5, []))))), .(.(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(7, .(6, .(5, .(4, .(5, .(6, .(7, .(6, .(5, []))))))))))))))))), .(.(5, .(5, .(5, .(4, .(5, .(5, .(5, .(6, .(6, .(6, .(5, .(5, .(4, []))))))))))))), .(.(1, .(2, .(2, .(2, .(1, .(1, .(3, .(2, .(3, .(2, .(3, .(3, .(3, []))))))))))))), .([], .(.(3, .(4, [])), .(.(4, .(5, .(5, .(5, .(5, []))))), .(.(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(7, .(6, .(5, .(4, .(5, .(6, .(7, .(6, .(5, []))))))))))))))))), .(.(5, .(5, .(5, .(4, .(5, .(5, .(5, .(6, .(6, .(6, .(5, .(5, .(4, []))))))))))))), .(.(1, .(2, .(2, .(2, .(1, .(1, .(3, .(2, .(3, .(2, .(3, .(3, .(3, []))))))))))))), .(.(3, .(4, [])), .(.(4, .(5, .(5, .(5, .(5, []))))), .(.(1, .(2, .(3, .(4, .(5, .(6, .(7, .(8, .(7, .(6, .(5, .(4, .(5, .(6, .(7, .(6, .(5, []))))))))))))))))), .(.(5, .(5, .(5, .(4, .(5, .(5, .(5, .(6, .(6, .(6, .(5, .(5, .(4, []))))))))))))), .(.(1, .(2, .(2, .(2, .(1, .(1, .(3, .(2, .(3, .(2, .(3, .(3, .(3, []))))))))))))), .(.(5, []), .(.(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, .(1, []))))))))))))))))))))))))), []))))))))))))))))))))))))))))).
if(X, Y, A, Z, B, W) :- ','(call1(X, Y, A, Z, B), is(W, +(A, B))).
if1(X, Z, W1, Y, W) :- ','(call2(X, Z, W1), addx(X, Y, W1, W)).
call1(X, Y, A, Z, B) :- ','(count(X, Y, A), occur(X, Z, B)).
call2(X, Z, W1) :- count(X, Z, W1).
=(X, X).
is(X0, X1).
=\=(X0, X1).
Query: occurall(g,g,a)
(11) PrologToPiTRSProof (SOUND transformation)
We use the technique of [TOCL09]. With regard to the inferred argument filtering the predicates were used in the following modes:
occurall_in: (b,b,f)
occur_in: (b,b,f)
if_in: (b,b,f,b,f,f)
call1_in: (b,b,f,b,f)
count_in: (b,b,f)
if1_in: (b,b,f,b,f)
call2_in: (b,b,f)
addx_in: (b,b,f,f)
Transforming
Prolog into the following
Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
occurall_in_gga([], X, []) → occurall_out_gga([], X, [])
occurall_in_gga(.(X, Y), Z, .(.(X, .(W, [])), V)) → U5_gga(X, Y, Z, W, V, occur_in_gga(X, Z, W))
occur_in_gga(X, [], 0) → occur_out_gga(X, [], 0)
occur_in_gga(X, .(Y, Z), W) → U1_gga(X, Y, Z, W, if_in_ggagaa(X, Y, A, Z, B, W))
if_in_ggagaa(X, Y, A, Z, B, W) → U9_ggagaa(X, Y, A, Z, B, W, call1_in_ggaga(X, Y, A, Z, B))
call1_in_ggaga(X, Y, A, Z, B) → U13_ggaga(X, Y, A, Z, B, count_in_gga(X, Y, A))
count_in_gga(X, [], 0) → count_out_gga(X, [], 0)
count_in_gga(X, .(Y, Z), W) → U2_gga(X, Y, Z, W, if1_in_ggaga(X, Z, W1, Y, W))
if1_in_ggaga(X, Z, W1, Y, W) → U11_ggaga(X, Z, W1, Y, W, call2_in_gga(X, Z, W1))
call2_in_gga(X, Z, W1) → U15_gga(X, Z, W1, count_in_gga(X, Z, W1))
U15_gga(X, Z, W1, count_out_gga(X, Z, W1)) → call2_out_gga(X, Z, W1)
U11_ggaga(X, Z, W1, Y, W, call2_out_gga(X, Z, W1)) → U12_ggaga(X, Z, W1, Y, W, addx_in_ggaa(X, Y, W1, W))
addx_in_ggaa(X, X, W1, W) → U3_ggaa(X, W1, W, is_in_aa(W, +(W1, 1)))
is_in_aa(X0, X1) → is_out_aa(X0, X1)
U3_ggaa(X, W1, W, is_out_aa(W, +(W1, 1))) → addx_out_ggaa(X, X, W1, W)
addx_in_ggaa(X, Y, W1, W1) → U4_ggaa(X, Y, W1, =\=_in_gg(X, Y))
=\=_in_gg(X0, X1) → =\=_out_gg(X0, X1)
U4_ggaa(X, Y, W1, =\=_out_gg(X, Y)) → addx_out_ggaa(X, Y, W1, W1)
U12_ggaga(X, Z, W1, Y, W, addx_out_ggaa(X, Y, W1, W)) → if1_out_ggaga(X, Z, W1, Y, W)
U2_gga(X, Y, Z, W, if1_out_ggaga(X, Z, W1, Y, W)) → count_out_gga(X, .(Y, Z), W)
U13_ggaga(X, Y, A, Z, B, count_out_gga(X, Y, A)) → U14_ggaga(X, Y, A, Z, B, occur_in_gga(X, Z, B))
U14_ggaga(X, Y, A, Z, B, occur_out_gga(X, Z, B)) → call1_out_ggaga(X, Y, A, Z, B)
U9_ggagaa(X, Y, A, Z, B, W, call1_out_ggaga(X, Y, A, Z, B)) → U10_ggagaa(X, Y, A, Z, B, W, is_in_aa(W, +(A, B)))
U10_ggagaa(X, Y, A, Z, B, W, is_out_aa(W, +(A, B))) → if_out_ggagaa(X, Y, A, Z, B, W)
U1_gga(X, Y, Z, W, if_out_ggagaa(X, Y, A, Z, B, W)) → occur_out_gga(X, .(Y, Z), W)
U5_gga(X, Y, Z, W, V, occur_out_gga(X, Z, W)) → U6_gga(X, Y, Z, W, V, occurall_in_gga(Y, Z, V))
U6_gga(X, Y, Z, W, V, occurall_out_gga(Y, Z, V)) → occurall_out_gga(.(X, Y), Z, .(.(X, .(W, [])), V))
The argument filtering Pi contains the following mapping:
occurall_in_gga(
x1,
x2,
x3) =
occurall_in_gga(
x1,
x2)
[] =
[]
occurall_out_gga(
x1,
x2,
x3) =
occurall_out_gga
.(
x1,
x2) =
.(
x1,
x2)
U5_gga(
x1,
x2,
x3,
x4,
x5,
x6) =
U5_gga(
x2,
x3,
x6)
occur_in_gga(
x1,
x2,
x3) =
occur_in_gga(
x1,
x2)
occur_out_gga(
x1,
x2,
x3) =
occur_out_gga
U1_gga(
x1,
x2,
x3,
x4,
x5) =
U1_gga(
x5)
if_in_ggagaa(
x1,
x2,
x3,
x4,
x5,
x6) =
if_in_ggagaa(
x1,
x2,
x4)
U9_ggagaa(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U9_ggagaa(
x7)
call1_in_ggaga(
x1,
x2,
x3,
x4,
x5) =
call1_in_ggaga(
x1,
x2,
x4)
U13_ggaga(
x1,
x2,
x3,
x4,
x5,
x6) =
U13_ggaga(
x1,
x4,
x6)
count_in_gga(
x1,
x2,
x3) =
count_in_gga(
x1,
x2)
count_out_gga(
x1,
x2,
x3) =
count_out_gga
U2_gga(
x1,
x2,
x3,
x4,
x5) =
U2_gga(
x5)
if1_in_ggaga(
x1,
x2,
x3,
x4,
x5) =
if1_in_ggaga(
x1,
x2,
x4)
U11_ggaga(
x1,
x2,
x3,
x4,
x5,
x6) =
U11_ggaga(
x1,
x4,
x6)
call2_in_gga(
x1,
x2,
x3) =
call2_in_gga(
x1,
x2)
U15_gga(
x1,
x2,
x3,
x4) =
U15_gga(
x4)
call2_out_gga(
x1,
x2,
x3) =
call2_out_gga
U12_ggaga(
x1,
x2,
x3,
x4,
x5,
x6) =
U12_ggaga(
x6)
+(
x1,
x2) =
+(
x1,
x2)
1 =
1
=\=_in_gg(
x1,
x2) =
=\=_in_gg(
x1,
x2)
=\=_out_gg(
x1,
x2) =
=\=_out_gg
if1_out_ggaga(
x1,
x2,
x3,
x4,
x5) =
if1_out_ggaga
addx_in_ggaa(
x1,
x2,
x3,
x4) =
addx_in_ggaa(
x1,
x2)
U3_ggaa(
x1,
x2,
x3,
x4) =
U3_ggaa(
x4)
is_in_aa(
x1,
x2) =
is_in_aa
is_out_aa(
x1,
x2) =
is_out_aa
addx_out_ggaa(
x1,
x2,
x3,
x4) =
addx_out_ggaa
U4_ggaa(
x1,
x2,
x3,
x4) =
U4_ggaa(
x4)
U14_ggaga(
x1,
x2,
x3,
x4,
x5,
x6) =
U14_ggaga(
x6)
call1_out_ggaga(
x1,
x2,
x3,
x4,
x5) =
call1_out_ggaga
U10_ggagaa(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U10_ggagaa(
x7)
if_out_ggagaa(
x1,
x2,
x3,
x4,
x5,
x6) =
if_out_ggagaa
U6_gga(
x1,
x2,
x3,
x4,
x5,
x6) =
U6_gga(
x6)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(12) Obligation:
Pi-finite rewrite system:
The TRS R consists of the following rules:
occurall_in_gga([], X, []) → occurall_out_gga([], X, [])
occurall_in_gga(.(X, Y), Z, .(.(X, .(W, [])), V)) → U5_gga(X, Y, Z, W, V, occur_in_gga(X, Z, W))
occur_in_gga(X, [], 0) → occur_out_gga(X, [], 0)
occur_in_gga(X, .(Y, Z), W) → U1_gga(X, Y, Z, W, if_in_ggagaa(X, Y, A, Z, B, W))
if_in_ggagaa(X, Y, A, Z, B, W) → U9_ggagaa(X, Y, A, Z, B, W, call1_in_ggaga(X, Y, A, Z, B))
call1_in_ggaga(X, Y, A, Z, B) → U13_ggaga(X, Y, A, Z, B, count_in_gga(X, Y, A))
count_in_gga(X, [], 0) → count_out_gga(X, [], 0)
count_in_gga(X, .(Y, Z), W) → U2_gga(X, Y, Z, W, if1_in_ggaga(X, Z, W1, Y, W))
if1_in_ggaga(X, Z, W1, Y, W) → U11_ggaga(X, Z, W1, Y, W, call2_in_gga(X, Z, W1))
call2_in_gga(X, Z, W1) → U15_gga(X, Z, W1, count_in_gga(X, Z, W1))
U15_gga(X, Z, W1, count_out_gga(X, Z, W1)) → call2_out_gga(X, Z, W1)
U11_ggaga(X, Z, W1, Y, W, call2_out_gga(X, Z, W1)) → U12_ggaga(X, Z, W1, Y, W, addx_in_ggaa(X, Y, W1, W))
addx_in_ggaa(X, X, W1, W) → U3_ggaa(X, W1, W, is_in_aa(W, +(W1, 1)))
is_in_aa(X0, X1) → is_out_aa(X0, X1)
U3_ggaa(X, W1, W, is_out_aa(W, +(W1, 1))) → addx_out_ggaa(X, X, W1, W)
addx_in_ggaa(X, Y, W1, W1) → U4_ggaa(X, Y, W1, =\=_in_gg(X, Y))
=\=_in_gg(X0, X1) → =\=_out_gg(X0, X1)
U4_ggaa(X, Y, W1, =\=_out_gg(X, Y)) → addx_out_ggaa(X, Y, W1, W1)
U12_ggaga(X, Z, W1, Y, W, addx_out_ggaa(X, Y, W1, W)) → if1_out_ggaga(X, Z, W1, Y, W)
U2_gga(X, Y, Z, W, if1_out_ggaga(X, Z, W1, Y, W)) → count_out_gga(X, .(Y, Z), W)
U13_ggaga(X, Y, A, Z, B, count_out_gga(X, Y, A)) → U14_ggaga(X, Y, A, Z, B, occur_in_gga(X, Z, B))
U14_ggaga(X, Y, A, Z, B, occur_out_gga(X, Z, B)) → call1_out_ggaga(X, Y, A, Z, B)
U9_ggagaa(X, Y, A, Z, B, W, call1_out_ggaga(X, Y, A, Z, B)) → U10_ggagaa(X, Y, A, Z, B, W, is_in_aa(W, +(A, B)))
U10_ggagaa(X, Y, A, Z, B, W, is_out_aa(W, +(A, B))) → if_out_ggagaa(X, Y, A, Z, B, W)
U1_gga(X, Y, Z, W, if_out_ggagaa(X, Y, A, Z, B, W)) → occur_out_gga(X, .(Y, Z), W)
U5_gga(X, Y, Z, W, V, occur_out_gga(X, Z, W)) → U6_gga(X, Y, Z, W, V, occurall_in_gga(Y, Z, V))
U6_gga(X, Y, Z, W, V, occurall_out_gga(Y, Z, V)) → occurall_out_gga(.(X, Y), Z, .(.(X, .(W, [])), V))
The argument filtering Pi contains the following mapping:
occurall_in_gga(
x1,
x2,
x3) =
occurall_in_gga(
x1,
x2)
[] =
[]
occurall_out_gga(
x1,
x2,
x3) =
occurall_out_gga
.(
x1,
x2) =
.(
x1,
x2)
U5_gga(
x1,
x2,
x3,
x4,
x5,
x6) =
U5_gga(
x2,
x3,
x6)
occur_in_gga(
x1,
x2,
x3) =
occur_in_gga(
x1,
x2)
occur_out_gga(
x1,
x2,
x3) =
occur_out_gga
U1_gga(
x1,
x2,
x3,
x4,
x5) =
U1_gga(
x5)
if_in_ggagaa(
x1,
x2,
x3,
x4,
x5,
x6) =
if_in_ggagaa(
x1,
x2,
x4)
U9_ggagaa(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U9_ggagaa(
x7)
call1_in_ggaga(
x1,
x2,
x3,
x4,
x5) =
call1_in_ggaga(
x1,
x2,
x4)
U13_ggaga(
x1,
x2,
x3,
x4,
x5,
x6) =
U13_ggaga(
x1,
x4,
x6)
count_in_gga(
x1,
x2,
x3) =
count_in_gga(
x1,
x2)
count_out_gga(
x1,
x2,
x3) =
count_out_gga
U2_gga(
x1,
x2,
x3,
x4,
x5) =
U2_gga(
x5)
if1_in_ggaga(
x1,
x2,
x3,
x4,
x5) =
if1_in_ggaga(
x1,
x2,
x4)
U11_ggaga(
x1,
x2,
x3,
x4,
x5,
x6) =
U11_ggaga(
x1,
x4,
x6)
call2_in_gga(
x1,
x2,
x3) =
call2_in_gga(
x1,
x2)
U15_gga(
x1,
x2,
x3,
x4) =
U15_gga(
x4)
call2_out_gga(
x1,
x2,
x3) =
call2_out_gga
U12_ggaga(
x1,
x2,
x3,
x4,
x5,
x6) =
U12_ggaga(
x6)
+(
x1,
x2) =
+(
x1,
x2)
1 =
1
=\=_in_gg(
x1,
x2) =
=\=_in_gg(
x1,
x2)
=\=_out_gg(
x1,
x2) =
=\=_out_gg
if1_out_ggaga(
x1,
x2,
x3,
x4,
x5) =
if1_out_ggaga
addx_in_ggaa(
x1,
x2,
x3,
x4) =
addx_in_ggaa(
x1,
x2)
U3_ggaa(
x1,
x2,
x3,
x4) =
U3_ggaa(
x4)
is_in_aa(
x1,
x2) =
is_in_aa
is_out_aa(
x1,
x2) =
is_out_aa
addx_out_ggaa(
x1,
x2,
x3,
x4) =
addx_out_ggaa
U4_ggaa(
x1,
x2,
x3,
x4) =
U4_ggaa(
x4)
U14_ggaga(
x1,
x2,
x3,
x4,
x5,
x6) =
U14_ggaga(
x6)
call1_out_ggaga(
x1,
x2,
x3,
x4,
x5) =
call1_out_ggaga
U10_ggagaa(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U10_ggagaa(
x7)
if_out_ggagaa(
x1,
x2,
x3,
x4,
x5,
x6) =
if_out_ggagaa
U6_gga(
x1,
x2,
x3,
x4,
x5,
x6) =
U6_gga(
x6)
(13) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:
OCCURALL_IN_GGA(.(X, Y), Z, .(.(X, .(W, [])), V)) → U5_GGA(X, Y, Z, W, V, occur_in_gga(X, Z, W))
OCCURALL_IN_GGA(.(X, Y), Z, .(.(X, .(W, [])), V)) → OCCUR_IN_GGA(X, Z, W)
OCCUR_IN_GGA(X, .(Y, Z), W) → U1_GGA(X, Y, Z, W, if_in_ggagaa(X, Y, A, Z, B, W))
OCCUR_IN_GGA(X, .(Y, Z), W) → IF_IN_GGAGAA(X, Y, A, Z, B, W)
IF_IN_GGAGAA(X, Y, A, Z, B, W) → U9_GGAGAA(X, Y, A, Z, B, W, call1_in_ggaga(X, Y, A, Z, B))
IF_IN_GGAGAA(X, Y, A, Z, B, W) → CALL1_IN_GGAGA(X, Y, A, Z, B)
CALL1_IN_GGAGA(X, Y, A, Z, B) → U13_GGAGA(X, Y, A, Z, B, count_in_gga(X, Y, A))
CALL1_IN_GGAGA(X, Y, A, Z, B) → COUNT_IN_GGA(X, Y, A)
COUNT_IN_GGA(X, .(Y, Z), W) → U2_GGA(X, Y, Z, W, if1_in_ggaga(X, Z, W1, Y, W))
COUNT_IN_GGA(X, .(Y, Z), W) → IF1_IN_GGAGA(X, Z, W1, Y, W)
IF1_IN_GGAGA(X, Z, W1, Y, W) → U11_GGAGA(X, Z, W1, Y, W, call2_in_gga(X, Z, W1))
IF1_IN_GGAGA(X, Z, W1, Y, W) → CALL2_IN_GGA(X, Z, W1)
CALL2_IN_GGA(X, Z, W1) → U15_GGA(X, Z, W1, count_in_gga(X, Z, W1))
CALL2_IN_GGA(X, Z, W1) → COUNT_IN_GGA(X, Z, W1)
U11_GGAGA(X, Z, W1, Y, W, call2_out_gga(X, Z, W1)) → U12_GGAGA(X, Z, W1, Y, W, addx_in_ggaa(X, Y, W1, W))
U11_GGAGA(X, Z, W1, Y, W, call2_out_gga(X, Z, W1)) → ADDX_IN_GGAA(X, Y, W1, W)
ADDX_IN_GGAA(X, X, W1, W) → U3_GGAA(X, W1, W, is_in_aa(W, +(W1, 1)))
ADDX_IN_GGAA(X, X, W1, W) → IS_IN_AA(W, +(W1, 1))
ADDX_IN_GGAA(X, Y, W1, W1) → U4_GGAA(X, Y, W1, =\=_in_gg(X, Y))
ADDX_IN_GGAA(X, Y, W1, W1) → =\=_IN_GG(X, Y)
U13_GGAGA(X, Y, A, Z, B, count_out_gga(X, Y, A)) → U14_GGAGA(X, Y, A, Z, B, occur_in_gga(X, Z, B))
U13_GGAGA(X, Y, A, Z, B, count_out_gga(X, Y, A)) → OCCUR_IN_GGA(X, Z, B)
U9_GGAGAA(X, Y, A, Z, B, W, call1_out_ggaga(X, Y, A, Z, B)) → U10_GGAGAA(X, Y, A, Z, B, W, is_in_aa(W, +(A, B)))
U9_GGAGAA(X, Y, A, Z, B, W, call1_out_ggaga(X, Y, A, Z, B)) → IS_IN_AA(W, +(A, B))
U5_GGA(X, Y, Z, W, V, occur_out_gga(X, Z, W)) → U6_GGA(X, Y, Z, W, V, occurall_in_gga(Y, Z, V))
U5_GGA(X, Y, Z, W, V, occur_out_gga(X, Z, W)) → OCCURALL_IN_GGA(Y, Z, V)
The TRS R consists of the following rules:
occurall_in_gga([], X, []) → occurall_out_gga([], X, [])
occurall_in_gga(.(X, Y), Z, .(.(X, .(W, [])), V)) → U5_gga(X, Y, Z, W, V, occur_in_gga(X, Z, W))
occur_in_gga(X, [], 0) → occur_out_gga(X, [], 0)
occur_in_gga(X, .(Y, Z), W) → U1_gga(X, Y, Z, W, if_in_ggagaa(X, Y, A, Z, B, W))
if_in_ggagaa(X, Y, A, Z, B, W) → U9_ggagaa(X, Y, A, Z, B, W, call1_in_ggaga(X, Y, A, Z, B))
call1_in_ggaga(X, Y, A, Z, B) → U13_ggaga(X, Y, A, Z, B, count_in_gga(X, Y, A))
count_in_gga(X, [], 0) → count_out_gga(X, [], 0)
count_in_gga(X, .(Y, Z), W) → U2_gga(X, Y, Z, W, if1_in_ggaga(X, Z, W1, Y, W))
if1_in_ggaga(X, Z, W1, Y, W) → U11_ggaga(X, Z, W1, Y, W, call2_in_gga(X, Z, W1))
call2_in_gga(X, Z, W1) → U15_gga(X, Z, W1, count_in_gga(X, Z, W1))
U15_gga(X, Z, W1, count_out_gga(X, Z, W1)) → call2_out_gga(X, Z, W1)
U11_ggaga(X, Z, W1, Y, W, call2_out_gga(X, Z, W1)) → U12_ggaga(X, Z, W1, Y, W, addx_in_ggaa(X, Y, W1, W))
addx_in_ggaa(X, X, W1, W) → U3_ggaa(X, W1, W, is_in_aa(W, +(W1, 1)))
is_in_aa(X0, X1) → is_out_aa(X0, X1)
U3_ggaa(X, W1, W, is_out_aa(W, +(W1, 1))) → addx_out_ggaa(X, X, W1, W)
addx_in_ggaa(X, Y, W1, W1) → U4_ggaa(X, Y, W1, =\=_in_gg(X, Y))
=\=_in_gg(X0, X1) → =\=_out_gg(X0, X1)
U4_ggaa(X, Y, W1, =\=_out_gg(X, Y)) → addx_out_ggaa(X, Y, W1, W1)
U12_ggaga(X, Z, W1, Y, W, addx_out_ggaa(X, Y, W1, W)) → if1_out_ggaga(X, Z, W1, Y, W)
U2_gga(X, Y, Z, W, if1_out_ggaga(X, Z, W1, Y, W)) → count_out_gga(X, .(Y, Z), W)
U13_ggaga(X, Y, A, Z, B, count_out_gga(X, Y, A)) → U14_ggaga(X, Y, A, Z, B, occur_in_gga(X, Z, B))
U14_ggaga(X, Y, A, Z, B, occur_out_gga(X, Z, B)) → call1_out_ggaga(X, Y, A, Z, B)
U9_ggagaa(X, Y, A, Z, B, W, call1_out_ggaga(X, Y, A, Z, B)) → U10_ggagaa(X, Y, A, Z, B, W, is_in_aa(W, +(A, B)))
U10_ggagaa(X, Y, A, Z, B, W, is_out_aa(W, +(A, B))) → if_out_ggagaa(X, Y, A, Z, B, W)
U1_gga(X, Y, Z, W, if_out_ggagaa(X, Y, A, Z, B, W)) → occur_out_gga(X, .(Y, Z), W)
U5_gga(X, Y, Z, W, V, occur_out_gga(X, Z, W)) → U6_gga(X, Y, Z, W, V, occurall_in_gga(Y, Z, V))
U6_gga(X, Y, Z, W, V, occurall_out_gga(Y, Z, V)) → occurall_out_gga(.(X, Y), Z, .(.(X, .(W, [])), V))
The argument filtering Pi contains the following mapping:
occurall_in_gga(
x1,
x2,
x3) =
occurall_in_gga(
x1,
x2)
[] =
[]
occurall_out_gga(
x1,
x2,
x3) =
occurall_out_gga
.(
x1,
x2) =
.(
x1,
x2)
U5_gga(
x1,
x2,
x3,
x4,
x5,
x6) =
U5_gga(
x2,
x3,
x6)
occur_in_gga(
x1,
x2,
x3) =
occur_in_gga(
x1,
x2)
occur_out_gga(
x1,
x2,
x3) =
occur_out_gga
U1_gga(
x1,
x2,
x3,
x4,
x5) =
U1_gga(
x5)
if_in_ggagaa(
x1,
x2,
x3,
x4,
x5,
x6) =
if_in_ggagaa(
x1,
x2,
x4)
U9_ggagaa(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U9_ggagaa(
x7)
call1_in_ggaga(
x1,
x2,
x3,
x4,
x5) =
call1_in_ggaga(
x1,
x2,
x4)
U13_ggaga(
x1,
x2,
x3,
x4,
x5,
x6) =
U13_ggaga(
x1,
x4,
x6)
count_in_gga(
x1,
x2,
x3) =
count_in_gga(
x1,
x2)
count_out_gga(
x1,
x2,
x3) =
count_out_gga
U2_gga(
x1,
x2,
x3,
x4,
x5) =
U2_gga(
x5)
if1_in_ggaga(
x1,
x2,
x3,
x4,
x5) =
if1_in_ggaga(
x1,
x2,
x4)
U11_ggaga(
x1,
x2,
x3,
x4,
x5,
x6) =
U11_ggaga(
x1,
x4,
x6)
call2_in_gga(
x1,
x2,
x3) =
call2_in_gga(
x1,
x2)
U15_gga(
x1,
x2,
x3,
x4) =
U15_gga(
x4)
call2_out_gga(
x1,
x2,
x3) =
call2_out_gga
U12_ggaga(
x1,
x2,
x3,
x4,
x5,
x6) =
U12_ggaga(
x6)
+(
x1,
x2) =
+(
x1,
x2)
1 =
1
=\=_in_gg(
x1,
x2) =
=\=_in_gg(
x1,
x2)
=\=_out_gg(
x1,
x2) =
=\=_out_gg
if1_out_ggaga(
x1,
x2,
x3,
x4,
x5) =
if1_out_ggaga
addx_in_ggaa(
x1,
x2,
x3,
x4) =
addx_in_ggaa(
x1,
x2)
U3_ggaa(
x1,
x2,
x3,
x4) =
U3_ggaa(
x4)
is_in_aa(
x1,
x2) =
is_in_aa
is_out_aa(
x1,
x2) =
is_out_aa
addx_out_ggaa(
x1,
x2,
x3,
x4) =
addx_out_ggaa
U4_ggaa(
x1,
x2,
x3,
x4) =
U4_ggaa(
x4)
U14_ggaga(
x1,
x2,
x3,
x4,
x5,
x6) =
U14_ggaga(
x6)
call1_out_ggaga(
x1,
x2,
x3,
x4,
x5) =
call1_out_ggaga
U10_ggagaa(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U10_ggagaa(
x7)
if_out_ggagaa(
x1,
x2,
x3,
x4,
x5,
x6) =
if_out_ggagaa
U6_gga(
x1,
x2,
x3,
x4,
x5,
x6) =
U6_gga(
x6)
OCCURALL_IN_GGA(
x1,
x2,
x3) =
OCCURALL_IN_GGA(
x1,
x2)
U5_GGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U5_GGA(
x2,
x3,
x6)
OCCUR_IN_GGA(
x1,
x2,
x3) =
OCCUR_IN_GGA(
x1,
x2)
U1_GGA(
x1,
x2,
x3,
x4,
x5) =
U1_GGA(
x5)
IF_IN_GGAGAA(
x1,
x2,
x3,
x4,
x5,
x6) =
IF_IN_GGAGAA(
x1,
x2,
x4)
U9_GGAGAA(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U9_GGAGAA(
x7)
CALL1_IN_GGAGA(
x1,
x2,
x3,
x4,
x5) =
CALL1_IN_GGAGA(
x1,
x2,
x4)
U13_GGAGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U13_GGAGA(
x1,
x4,
x6)
COUNT_IN_GGA(
x1,
x2,
x3) =
COUNT_IN_GGA(
x1,
x2)
U2_GGA(
x1,
x2,
x3,
x4,
x5) =
U2_GGA(
x5)
IF1_IN_GGAGA(
x1,
x2,
x3,
x4,
x5) =
IF1_IN_GGAGA(
x1,
x2,
x4)
U11_GGAGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U11_GGAGA(
x1,
x4,
x6)
CALL2_IN_GGA(
x1,
x2,
x3) =
CALL2_IN_GGA(
x1,
x2)
U15_GGA(
x1,
x2,
x3,
x4) =
U15_GGA(
x4)
U12_GGAGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U12_GGAGA(
x6)
ADDX_IN_GGAA(
x1,
x2,
x3,
x4) =
ADDX_IN_GGAA(
x1,
x2)
U3_GGAA(
x1,
x2,
x3,
x4) =
U3_GGAA(
x4)
IS_IN_AA(
x1,
x2) =
IS_IN_AA
U4_GGAA(
x1,
x2,
x3,
x4) =
U4_GGAA(
x4)
=\=_IN_GG(
x1,
x2) =
=\=_IN_GG(
x1,
x2)
U14_GGAGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U14_GGAGA(
x6)
U10_GGAGAA(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U10_GGAGAA(
x7)
U6_GGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U6_GGA(
x6)
We have to consider all (P,R,Pi)-chains
(14) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
OCCURALL_IN_GGA(.(X, Y), Z, .(.(X, .(W, [])), V)) → U5_GGA(X, Y, Z, W, V, occur_in_gga(X, Z, W))
OCCURALL_IN_GGA(.(X, Y), Z, .(.(X, .(W, [])), V)) → OCCUR_IN_GGA(X, Z, W)
OCCUR_IN_GGA(X, .(Y, Z), W) → U1_GGA(X, Y, Z, W, if_in_ggagaa(X, Y, A, Z, B, W))
OCCUR_IN_GGA(X, .(Y, Z), W) → IF_IN_GGAGAA(X, Y, A, Z, B, W)
IF_IN_GGAGAA(X, Y, A, Z, B, W) → U9_GGAGAA(X, Y, A, Z, B, W, call1_in_ggaga(X, Y, A, Z, B))
IF_IN_GGAGAA(X, Y, A, Z, B, W) → CALL1_IN_GGAGA(X, Y, A, Z, B)
CALL1_IN_GGAGA(X, Y, A, Z, B) → U13_GGAGA(X, Y, A, Z, B, count_in_gga(X, Y, A))
CALL1_IN_GGAGA(X, Y, A, Z, B) → COUNT_IN_GGA(X, Y, A)
COUNT_IN_GGA(X, .(Y, Z), W) → U2_GGA(X, Y, Z, W, if1_in_ggaga(X, Z, W1, Y, W))
COUNT_IN_GGA(X, .(Y, Z), W) → IF1_IN_GGAGA(X, Z, W1, Y, W)
IF1_IN_GGAGA(X, Z, W1, Y, W) → U11_GGAGA(X, Z, W1, Y, W, call2_in_gga(X, Z, W1))
IF1_IN_GGAGA(X, Z, W1, Y, W) → CALL2_IN_GGA(X, Z, W1)
CALL2_IN_GGA(X, Z, W1) → U15_GGA(X, Z, W1, count_in_gga(X, Z, W1))
CALL2_IN_GGA(X, Z, W1) → COUNT_IN_GGA(X, Z, W1)
U11_GGAGA(X, Z, W1, Y, W, call2_out_gga(X, Z, W1)) → U12_GGAGA(X, Z, W1, Y, W, addx_in_ggaa(X, Y, W1, W))
U11_GGAGA(X, Z, W1, Y, W, call2_out_gga(X, Z, W1)) → ADDX_IN_GGAA(X, Y, W1, W)
ADDX_IN_GGAA(X, X, W1, W) → U3_GGAA(X, W1, W, is_in_aa(W, +(W1, 1)))
ADDX_IN_GGAA(X, X, W1, W) → IS_IN_AA(W, +(W1, 1))
ADDX_IN_GGAA(X, Y, W1, W1) → U4_GGAA(X, Y, W1, =\=_in_gg(X, Y))
ADDX_IN_GGAA(X, Y, W1, W1) → =\=_IN_GG(X, Y)
U13_GGAGA(X, Y, A, Z, B, count_out_gga(X, Y, A)) → U14_GGAGA(X, Y, A, Z, B, occur_in_gga(X, Z, B))
U13_GGAGA(X, Y, A, Z, B, count_out_gga(X, Y, A)) → OCCUR_IN_GGA(X, Z, B)
U9_GGAGAA(X, Y, A, Z, B, W, call1_out_ggaga(X, Y, A, Z, B)) → U10_GGAGAA(X, Y, A, Z, B, W, is_in_aa(W, +(A, B)))
U9_GGAGAA(X, Y, A, Z, B, W, call1_out_ggaga(X, Y, A, Z, B)) → IS_IN_AA(W, +(A, B))
U5_GGA(X, Y, Z, W, V, occur_out_gga(X, Z, W)) → U6_GGA(X, Y, Z, W, V, occurall_in_gga(Y, Z, V))
U5_GGA(X, Y, Z, W, V, occur_out_gga(X, Z, W)) → OCCURALL_IN_GGA(Y, Z, V)
The TRS R consists of the following rules:
occurall_in_gga([], X, []) → occurall_out_gga([], X, [])
occurall_in_gga(.(X, Y), Z, .(.(X, .(W, [])), V)) → U5_gga(X, Y, Z, W, V, occur_in_gga(X, Z, W))
occur_in_gga(X, [], 0) → occur_out_gga(X, [], 0)
occur_in_gga(X, .(Y, Z), W) → U1_gga(X, Y, Z, W, if_in_ggagaa(X, Y, A, Z, B, W))
if_in_ggagaa(X, Y, A, Z, B, W) → U9_ggagaa(X, Y, A, Z, B, W, call1_in_ggaga(X, Y, A, Z, B))
call1_in_ggaga(X, Y, A, Z, B) → U13_ggaga(X, Y, A, Z, B, count_in_gga(X, Y, A))
count_in_gga(X, [], 0) → count_out_gga(X, [], 0)
count_in_gga(X, .(Y, Z), W) → U2_gga(X, Y, Z, W, if1_in_ggaga(X, Z, W1, Y, W))
if1_in_ggaga(X, Z, W1, Y, W) → U11_ggaga(X, Z, W1, Y, W, call2_in_gga(X, Z, W1))
call2_in_gga(X, Z, W1) → U15_gga(X, Z, W1, count_in_gga(X, Z, W1))
U15_gga(X, Z, W1, count_out_gga(X, Z, W1)) → call2_out_gga(X, Z, W1)
U11_ggaga(X, Z, W1, Y, W, call2_out_gga(X, Z, W1)) → U12_ggaga(X, Z, W1, Y, W, addx_in_ggaa(X, Y, W1, W))
addx_in_ggaa(X, X, W1, W) → U3_ggaa(X, W1, W, is_in_aa(W, +(W1, 1)))
is_in_aa(X0, X1) → is_out_aa(X0, X1)
U3_ggaa(X, W1, W, is_out_aa(W, +(W1, 1))) → addx_out_ggaa(X, X, W1, W)
addx_in_ggaa(X, Y, W1, W1) → U4_ggaa(X, Y, W1, =\=_in_gg(X, Y))
=\=_in_gg(X0, X1) → =\=_out_gg(X0, X1)
U4_ggaa(X, Y, W1, =\=_out_gg(X, Y)) → addx_out_ggaa(X, Y, W1, W1)
U12_ggaga(X, Z, W1, Y, W, addx_out_ggaa(X, Y, W1, W)) → if1_out_ggaga(X, Z, W1, Y, W)
U2_gga(X, Y, Z, W, if1_out_ggaga(X, Z, W1, Y, W)) → count_out_gga(X, .(Y, Z), W)
U13_ggaga(X, Y, A, Z, B, count_out_gga(X, Y, A)) → U14_ggaga(X, Y, A, Z, B, occur_in_gga(X, Z, B))
U14_ggaga(X, Y, A, Z, B, occur_out_gga(X, Z, B)) → call1_out_ggaga(X, Y, A, Z, B)
U9_ggagaa(X, Y, A, Z, B, W, call1_out_ggaga(X, Y, A, Z, B)) → U10_ggagaa(X, Y, A, Z, B, W, is_in_aa(W, +(A, B)))
U10_ggagaa(X, Y, A, Z, B, W, is_out_aa(W, +(A, B))) → if_out_ggagaa(X, Y, A, Z, B, W)
U1_gga(X, Y, Z, W, if_out_ggagaa(X, Y, A, Z, B, W)) → occur_out_gga(X, .(Y, Z), W)
U5_gga(X, Y, Z, W, V, occur_out_gga(X, Z, W)) → U6_gga(X, Y, Z, W, V, occurall_in_gga(Y, Z, V))
U6_gga(X, Y, Z, W, V, occurall_out_gga(Y, Z, V)) → occurall_out_gga(.(X, Y), Z, .(.(X, .(W, [])), V))
The argument filtering Pi contains the following mapping:
occurall_in_gga(
x1,
x2,
x3) =
occurall_in_gga(
x1,
x2)
[] =
[]
occurall_out_gga(
x1,
x2,
x3) =
occurall_out_gga
.(
x1,
x2) =
.(
x1,
x2)
U5_gga(
x1,
x2,
x3,
x4,
x5,
x6) =
U5_gga(
x2,
x3,
x6)
occur_in_gga(
x1,
x2,
x3) =
occur_in_gga(
x1,
x2)
occur_out_gga(
x1,
x2,
x3) =
occur_out_gga
U1_gga(
x1,
x2,
x3,
x4,
x5) =
U1_gga(
x5)
if_in_ggagaa(
x1,
x2,
x3,
x4,
x5,
x6) =
if_in_ggagaa(
x1,
x2,
x4)
U9_ggagaa(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U9_ggagaa(
x7)
call1_in_ggaga(
x1,
x2,
x3,
x4,
x5) =
call1_in_ggaga(
x1,
x2,
x4)
U13_ggaga(
x1,
x2,
x3,
x4,
x5,
x6) =
U13_ggaga(
x1,
x4,
x6)
count_in_gga(
x1,
x2,
x3) =
count_in_gga(
x1,
x2)
count_out_gga(
x1,
x2,
x3) =
count_out_gga
U2_gga(
x1,
x2,
x3,
x4,
x5) =
U2_gga(
x5)
if1_in_ggaga(
x1,
x2,
x3,
x4,
x5) =
if1_in_ggaga(
x1,
x2,
x4)
U11_ggaga(
x1,
x2,
x3,
x4,
x5,
x6) =
U11_ggaga(
x1,
x4,
x6)
call2_in_gga(
x1,
x2,
x3) =
call2_in_gga(
x1,
x2)
U15_gga(
x1,
x2,
x3,
x4) =
U15_gga(
x4)
call2_out_gga(
x1,
x2,
x3) =
call2_out_gga
U12_ggaga(
x1,
x2,
x3,
x4,
x5,
x6) =
U12_ggaga(
x6)
+(
x1,
x2) =
+(
x1,
x2)
1 =
1
=\=_in_gg(
x1,
x2) =
=\=_in_gg(
x1,
x2)
=\=_out_gg(
x1,
x2) =
=\=_out_gg
if1_out_ggaga(
x1,
x2,
x3,
x4,
x5) =
if1_out_ggaga
addx_in_ggaa(
x1,
x2,
x3,
x4) =
addx_in_ggaa(
x1,
x2)
U3_ggaa(
x1,
x2,
x3,
x4) =
U3_ggaa(
x4)
is_in_aa(
x1,
x2) =
is_in_aa
is_out_aa(
x1,
x2) =
is_out_aa
addx_out_ggaa(
x1,
x2,
x3,
x4) =
addx_out_ggaa
U4_ggaa(
x1,
x2,
x3,
x4) =
U4_ggaa(
x4)
U14_ggaga(
x1,
x2,
x3,
x4,
x5,
x6) =
U14_ggaga(
x6)
call1_out_ggaga(
x1,
x2,
x3,
x4,
x5) =
call1_out_ggaga
U10_ggagaa(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U10_ggagaa(
x7)
if_out_ggagaa(
x1,
x2,
x3,
x4,
x5,
x6) =
if_out_ggagaa
U6_gga(
x1,
x2,
x3,
x4,
x5,
x6) =
U6_gga(
x6)
OCCURALL_IN_GGA(
x1,
x2,
x3) =
OCCURALL_IN_GGA(
x1,
x2)
U5_GGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U5_GGA(
x2,
x3,
x6)
OCCUR_IN_GGA(
x1,
x2,
x3) =
OCCUR_IN_GGA(
x1,
x2)
U1_GGA(
x1,
x2,
x3,
x4,
x5) =
U1_GGA(
x5)
IF_IN_GGAGAA(
x1,
x2,
x3,
x4,
x5,
x6) =
IF_IN_GGAGAA(
x1,
x2,
x4)
U9_GGAGAA(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U9_GGAGAA(
x7)
CALL1_IN_GGAGA(
x1,
x2,
x3,
x4,
x5) =
CALL1_IN_GGAGA(
x1,
x2,
x4)
U13_GGAGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U13_GGAGA(
x1,
x4,
x6)
COUNT_IN_GGA(
x1,
x2,
x3) =
COUNT_IN_GGA(
x1,
x2)
U2_GGA(
x1,
x2,
x3,
x4,
x5) =
U2_GGA(
x5)
IF1_IN_GGAGA(
x1,
x2,
x3,
x4,
x5) =
IF1_IN_GGAGA(
x1,
x2,
x4)
U11_GGAGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U11_GGAGA(
x1,
x4,
x6)
CALL2_IN_GGA(
x1,
x2,
x3) =
CALL2_IN_GGA(
x1,
x2)
U15_GGA(
x1,
x2,
x3,
x4) =
U15_GGA(
x4)
U12_GGAGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U12_GGAGA(
x6)
ADDX_IN_GGAA(
x1,
x2,
x3,
x4) =
ADDX_IN_GGAA(
x1,
x2)
U3_GGAA(
x1,
x2,
x3,
x4) =
U3_GGAA(
x4)
IS_IN_AA(
x1,
x2) =
IS_IN_AA
U4_GGAA(
x1,
x2,
x3,
x4) =
U4_GGAA(
x4)
=\=_IN_GG(
x1,
x2) =
=\=_IN_GG(
x1,
x2)
U14_GGAGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U14_GGAGA(
x6)
U10_GGAGAA(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U10_GGAGAA(
x7)
U6_GGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U6_GGA(
x6)
We have to consider all (P,R,Pi)-chains
(15) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 17 less nodes.
(16) Complex Obligation (AND)
(17) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
COUNT_IN_GGA(X, .(Y, Z), W) → IF1_IN_GGAGA(X, Z, W1, Y, W)
IF1_IN_GGAGA(X, Z, W1, Y, W) → CALL2_IN_GGA(X, Z, W1)
CALL2_IN_GGA(X, Z, W1) → COUNT_IN_GGA(X, Z, W1)
The TRS R consists of the following rules:
occurall_in_gga([], X, []) → occurall_out_gga([], X, [])
occurall_in_gga(.(X, Y), Z, .(.(X, .(W, [])), V)) → U5_gga(X, Y, Z, W, V, occur_in_gga(X, Z, W))
occur_in_gga(X, [], 0) → occur_out_gga(X, [], 0)
occur_in_gga(X, .(Y, Z), W) → U1_gga(X, Y, Z, W, if_in_ggagaa(X, Y, A, Z, B, W))
if_in_ggagaa(X, Y, A, Z, B, W) → U9_ggagaa(X, Y, A, Z, B, W, call1_in_ggaga(X, Y, A, Z, B))
call1_in_ggaga(X, Y, A, Z, B) → U13_ggaga(X, Y, A, Z, B, count_in_gga(X, Y, A))
count_in_gga(X, [], 0) → count_out_gga(X, [], 0)
count_in_gga(X, .(Y, Z), W) → U2_gga(X, Y, Z, W, if1_in_ggaga(X, Z, W1, Y, W))
if1_in_ggaga(X, Z, W1, Y, W) → U11_ggaga(X, Z, W1, Y, W, call2_in_gga(X, Z, W1))
call2_in_gga(X, Z, W1) → U15_gga(X, Z, W1, count_in_gga(X, Z, W1))
U15_gga(X, Z, W1, count_out_gga(X, Z, W1)) → call2_out_gga(X, Z, W1)
U11_ggaga(X, Z, W1, Y, W, call2_out_gga(X, Z, W1)) → U12_ggaga(X, Z, W1, Y, W, addx_in_ggaa(X, Y, W1, W))
addx_in_ggaa(X, X, W1, W) → U3_ggaa(X, W1, W, is_in_aa(W, +(W1, 1)))
is_in_aa(X0, X1) → is_out_aa(X0, X1)
U3_ggaa(X, W1, W, is_out_aa(W, +(W1, 1))) → addx_out_ggaa(X, X, W1, W)
addx_in_ggaa(X, Y, W1, W1) → U4_ggaa(X, Y, W1, =\=_in_gg(X, Y))
=\=_in_gg(X0, X1) → =\=_out_gg(X0, X1)
U4_ggaa(X, Y, W1, =\=_out_gg(X, Y)) → addx_out_ggaa(X, Y, W1, W1)
U12_ggaga(X, Z, W1, Y, W, addx_out_ggaa(X, Y, W1, W)) → if1_out_ggaga(X, Z, W1, Y, W)
U2_gga(X, Y, Z, W, if1_out_ggaga(X, Z, W1, Y, W)) → count_out_gga(X, .(Y, Z), W)
U13_ggaga(X, Y, A, Z, B, count_out_gga(X, Y, A)) → U14_ggaga(X, Y, A, Z, B, occur_in_gga(X, Z, B))
U14_ggaga(X, Y, A, Z, B, occur_out_gga(X, Z, B)) → call1_out_ggaga(X, Y, A, Z, B)
U9_ggagaa(X, Y, A, Z, B, W, call1_out_ggaga(X, Y, A, Z, B)) → U10_ggagaa(X, Y, A, Z, B, W, is_in_aa(W, +(A, B)))
U10_ggagaa(X, Y, A, Z, B, W, is_out_aa(W, +(A, B))) → if_out_ggagaa(X, Y, A, Z, B, W)
U1_gga(X, Y, Z, W, if_out_ggagaa(X, Y, A, Z, B, W)) → occur_out_gga(X, .(Y, Z), W)
U5_gga(X, Y, Z, W, V, occur_out_gga(X, Z, W)) → U6_gga(X, Y, Z, W, V, occurall_in_gga(Y, Z, V))
U6_gga(X, Y, Z, W, V, occurall_out_gga(Y, Z, V)) → occurall_out_gga(.(X, Y), Z, .(.(X, .(W, [])), V))
The argument filtering Pi contains the following mapping:
occurall_in_gga(
x1,
x2,
x3) =
occurall_in_gga(
x1,
x2)
[] =
[]
occurall_out_gga(
x1,
x2,
x3) =
occurall_out_gga
.(
x1,
x2) =
.(
x1,
x2)
U5_gga(
x1,
x2,
x3,
x4,
x5,
x6) =
U5_gga(
x2,
x3,
x6)
occur_in_gga(
x1,
x2,
x3) =
occur_in_gga(
x1,
x2)
occur_out_gga(
x1,
x2,
x3) =
occur_out_gga
U1_gga(
x1,
x2,
x3,
x4,
x5) =
U1_gga(
x5)
if_in_ggagaa(
x1,
x2,
x3,
x4,
x5,
x6) =
if_in_ggagaa(
x1,
x2,
x4)
U9_ggagaa(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U9_ggagaa(
x7)
call1_in_ggaga(
x1,
x2,
x3,
x4,
x5) =
call1_in_ggaga(
x1,
x2,
x4)
U13_ggaga(
x1,
x2,
x3,
x4,
x5,
x6) =
U13_ggaga(
x1,
x4,
x6)
count_in_gga(
x1,
x2,
x3) =
count_in_gga(
x1,
x2)
count_out_gga(
x1,
x2,
x3) =
count_out_gga
U2_gga(
x1,
x2,
x3,
x4,
x5) =
U2_gga(
x5)
if1_in_ggaga(
x1,
x2,
x3,
x4,
x5) =
if1_in_ggaga(
x1,
x2,
x4)
U11_ggaga(
x1,
x2,
x3,
x4,
x5,
x6) =
U11_ggaga(
x1,
x4,
x6)
call2_in_gga(
x1,
x2,
x3) =
call2_in_gga(
x1,
x2)
U15_gga(
x1,
x2,
x3,
x4) =
U15_gga(
x4)
call2_out_gga(
x1,
x2,
x3) =
call2_out_gga
U12_ggaga(
x1,
x2,
x3,
x4,
x5,
x6) =
U12_ggaga(
x6)
+(
x1,
x2) =
+(
x1,
x2)
1 =
1
=\=_in_gg(
x1,
x2) =
=\=_in_gg(
x1,
x2)
=\=_out_gg(
x1,
x2) =
=\=_out_gg
if1_out_ggaga(
x1,
x2,
x3,
x4,
x5) =
if1_out_ggaga
addx_in_ggaa(
x1,
x2,
x3,
x4) =
addx_in_ggaa(
x1,
x2)
U3_ggaa(
x1,
x2,
x3,
x4) =
U3_ggaa(
x4)
is_in_aa(
x1,
x2) =
is_in_aa
is_out_aa(
x1,
x2) =
is_out_aa
addx_out_ggaa(
x1,
x2,
x3,
x4) =
addx_out_ggaa
U4_ggaa(
x1,
x2,
x3,
x4) =
U4_ggaa(
x4)
U14_ggaga(
x1,
x2,
x3,
x4,
x5,
x6) =
U14_ggaga(
x6)
call1_out_ggaga(
x1,
x2,
x3,
x4,
x5) =
call1_out_ggaga
U10_ggagaa(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U10_ggagaa(
x7)
if_out_ggagaa(
x1,
x2,
x3,
x4,
x5,
x6) =
if_out_ggagaa
U6_gga(
x1,
x2,
x3,
x4,
x5,
x6) =
U6_gga(
x6)
COUNT_IN_GGA(
x1,
x2,
x3) =
COUNT_IN_GGA(
x1,
x2)
IF1_IN_GGAGA(
x1,
x2,
x3,
x4,
x5) =
IF1_IN_GGAGA(
x1,
x2,
x4)
CALL2_IN_GGA(
x1,
x2,
x3) =
CALL2_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(18) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(19) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
COUNT_IN_GGA(X, .(Y, Z), W) → IF1_IN_GGAGA(X, Z, W1, Y, W)
IF1_IN_GGAGA(X, Z, W1, Y, W) → CALL2_IN_GGA(X, Z, W1)
CALL2_IN_GGA(X, Z, W1) → COUNT_IN_GGA(X, Z, W1)
R is empty.
The argument filtering Pi contains the following mapping:
.(
x1,
x2) =
.(
x1,
x2)
COUNT_IN_GGA(
x1,
x2,
x3) =
COUNT_IN_GGA(
x1,
x2)
IF1_IN_GGAGA(
x1,
x2,
x3,
x4,
x5) =
IF1_IN_GGAGA(
x1,
x2,
x4)
CALL2_IN_GGA(
x1,
x2,
x3) =
CALL2_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(20) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(21) Obligation:
Q DP problem:
The TRS P consists of the following rules:
COUNT_IN_GGA(X, .(Y, Z)) → IF1_IN_GGAGA(X, Z, Y)
IF1_IN_GGAGA(X, Z, Y) → CALL2_IN_GGA(X, Z)
CALL2_IN_GGA(X, Z) → COUNT_IN_GGA(X, Z)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(22) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- IF1_IN_GGAGA(X, Z, Y) → CALL2_IN_GGA(X, Z)
The graph contains the following edges 1 >= 1, 2 >= 2
- CALL2_IN_GGA(X, Z) → COUNT_IN_GGA(X, Z)
The graph contains the following edges 1 >= 1, 2 >= 2
- COUNT_IN_GGA(X, .(Y, Z)) → IF1_IN_GGAGA(X, Z, Y)
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3
(23) YES
(24) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
OCCUR_IN_GGA(X, .(Y, Z), W) → IF_IN_GGAGAA(X, Y, A, Z, B, W)
IF_IN_GGAGAA(X, Y, A, Z, B, W) → CALL1_IN_GGAGA(X, Y, A, Z, B)
CALL1_IN_GGAGA(X, Y, A, Z, B) → U13_GGAGA(X, Y, A, Z, B, count_in_gga(X, Y, A))
U13_GGAGA(X, Y, A, Z, B, count_out_gga(X, Y, A)) → OCCUR_IN_GGA(X, Z, B)
The TRS R consists of the following rules:
occurall_in_gga([], X, []) → occurall_out_gga([], X, [])
occurall_in_gga(.(X, Y), Z, .(.(X, .(W, [])), V)) → U5_gga(X, Y, Z, W, V, occur_in_gga(X, Z, W))
occur_in_gga(X, [], 0) → occur_out_gga(X, [], 0)
occur_in_gga(X, .(Y, Z), W) → U1_gga(X, Y, Z, W, if_in_ggagaa(X, Y, A, Z, B, W))
if_in_ggagaa(X, Y, A, Z, B, W) → U9_ggagaa(X, Y, A, Z, B, W, call1_in_ggaga(X, Y, A, Z, B))
call1_in_ggaga(X, Y, A, Z, B) → U13_ggaga(X, Y, A, Z, B, count_in_gga(X, Y, A))
count_in_gga(X, [], 0) → count_out_gga(X, [], 0)
count_in_gga(X, .(Y, Z), W) → U2_gga(X, Y, Z, W, if1_in_ggaga(X, Z, W1, Y, W))
if1_in_ggaga(X, Z, W1, Y, W) → U11_ggaga(X, Z, W1, Y, W, call2_in_gga(X, Z, W1))
call2_in_gga(X, Z, W1) → U15_gga(X, Z, W1, count_in_gga(X, Z, W1))
U15_gga(X, Z, W1, count_out_gga(X, Z, W1)) → call2_out_gga(X, Z, W1)
U11_ggaga(X, Z, W1, Y, W, call2_out_gga(X, Z, W1)) → U12_ggaga(X, Z, W1, Y, W, addx_in_ggaa(X, Y, W1, W))
addx_in_ggaa(X, X, W1, W) → U3_ggaa(X, W1, W, is_in_aa(W, +(W1, 1)))
is_in_aa(X0, X1) → is_out_aa(X0, X1)
U3_ggaa(X, W1, W, is_out_aa(W, +(W1, 1))) → addx_out_ggaa(X, X, W1, W)
addx_in_ggaa(X, Y, W1, W1) → U4_ggaa(X, Y, W1, =\=_in_gg(X, Y))
=\=_in_gg(X0, X1) → =\=_out_gg(X0, X1)
U4_ggaa(X, Y, W1, =\=_out_gg(X, Y)) → addx_out_ggaa(X, Y, W1, W1)
U12_ggaga(X, Z, W1, Y, W, addx_out_ggaa(X, Y, W1, W)) → if1_out_ggaga(X, Z, W1, Y, W)
U2_gga(X, Y, Z, W, if1_out_ggaga(X, Z, W1, Y, W)) → count_out_gga(X, .(Y, Z), W)
U13_ggaga(X, Y, A, Z, B, count_out_gga(X, Y, A)) → U14_ggaga(X, Y, A, Z, B, occur_in_gga(X, Z, B))
U14_ggaga(X, Y, A, Z, B, occur_out_gga(X, Z, B)) → call1_out_ggaga(X, Y, A, Z, B)
U9_ggagaa(X, Y, A, Z, B, W, call1_out_ggaga(X, Y, A, Z, B)) → U10_ggagaa(X, Y, A, Z, B, W, is_in_aa(W, +(A, B)))
U10_ggagaa(X, Y, A, Z, B, W, is_out_aa(W, +(A, B))) → if_out_ggagaa(X, Y, A, Z, B, W)
U1_gga(X, Y, Z, W, if_out_ggagaa(X, Y, A, Z, B, W)) → occur_out_gga(X, .(Y, Z), W)
U5_gga(X, Y, Z, W, V, occur_out_gga(X, Z, W)) → U6_gga(X, Y, Z, W, V, occurall_in_gga(Y, Z, V))
U6_gga(X, Y, Z, W, V, occurall_out_gga(Y, Z, V)) → occurall_out_gga(.(X, Y), Z, .(.(X, .(W, [])), V))
The argument filtering Pi contains the following mapping:
occurall_in_gga(
x1,
x2,
x3) =
occurall_in_gga(
x1,
x2)
[] =
[]
occurall_out_gga(
x1,
x2,
x3) =
occurall_out_gga
.(
x1,
x2) =
.(
x1,
x2)
U5_gga(
x1,
x2,
x3,
x4,
x5,
x6) =
U5_gga(
x2,
x3,
x6)
occur_in_gga(
x1,
x2,
x3) =
occur_in_gga(
x1,
x2)
occur_out_gga(
x1,
x2,
x3) =
occur_out_gga
U1_gga(
x1,
x2,
x3,
x4,
x5) =
U1_gga(
x5)
if_in_ggagaa(
x1,
x2,
x3,
x4,
x5,
x6) =
if_in_ggagaa(
x1,
x2,
x4)
U9_ggagaa(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U9_ggagaa(
x7)
call1_in_ggaga(
x1,
x2,
x3,
x4,
x5) =
call1_in_ggaga(
x1,
x2,
x4)
U13_ggaga(
x1,
x2,
x3,
x4,
x5,
x6) =
U13_ggaga(
x1,
x4,
x6)
count_in_gga(
x1,
x2,
x3) =
count_in_gga(
x1,
x2)
count_out_gga(
x1,
x2,
x3) =
count_out_gga
U2_gga(
x1,
x2,
x3,
x4,
x5) =
U2_gga(
x5)
if1_in_ggaga(
x1,
x2,
x3,
x4,
x5) =
if1_in_ggaga(
x1,
x2,
x4)
U11_ggaga(
x1,
x2,
x3,
x4,
x5,
x6) =
U11_ggaga(
x1,
x4,
x6)
call2_in_gga(
x1,
x2,
x3) =
call2_in_gga(
x1,
x2)
U15_gga(
x1,
x2,
x3,
x4) =
U15_gga(
x4)
call2_out_gga(
x1,
x2,
x3) =
call2_out_gga
U12_ggaga(
x1,
x2,
x3,
x4,
x5,
x6) =
U12_ggaga(
x6)
+(
x1,
x2) =
+(
x1,
x2)
1 =
1
=\=_in_gg(
x1,
x2) =
=\=_in_gg(
x1,
x2)
=\=_out_gg(
x1,
x2) =
=\=_out_gg
if1_out_ggaga(
x1,
x2,
x3,
x4,
x5) =
if1_out_ggaga
addx_in_ggaa(
x1,
x2,
x3,
x4) =
addx_in_ggaa(
x1,
x2)
U3_ggaa(
x1,
x2,
x3,
x4) =
U3_ggaa(
x4)
is_in_aa(
x1,
x2) =
is_in_aa
is_out_aa(
x1,
x2) =
is_out_aa
addx_out_ggaa(
x1,
x2,
x3,
x4) =
addx_out_ggaa
U4_ggaa(
x1,
x2,
x3,
x4) =
U4_ggaa(
x4)
U14_ggaga(
x1,
x2,
x3,
x4,
x5,
x6) =
U14_ggaga(
x6)
call1_out_ggaga(
x1,
x2,
x3,
x4,
x5) =
call1_out_ggaga
U10_ggagaa(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U10_ggagaa(
x7)
if_out_ggagaa(
x1,
x2,
x3,
x4,
x5,
x6) =
if_out_ggagaa
U6_gga(
x1,
x2,
x3,
x4,
x5,
x6) =
U6_gga(
x6)
OCCUR_IN_GGA(
x1,
x2,
x3) =
OCCUR_IN_GGA(
x1,
x2)
IF_IN_GGAGAA(
x1,
x2,
x3,
x4,
x5,
x6) =
IF_IN_GGAGAA(
x1,
x2,
x4)
CALL1_IN_GGAGA(
x1,
x2,
x3,
x4,
x5) =
CALL1_IN_GGAGA(
x1,
x2,
x4)
U13_GGAGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U13_GGAGA(
x1,
x4,
x6)
We have to consider all (P,R,Pi)-chains
(25) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(26) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
OCCUR_IN_GGA(X, .(Y, Z), W) → IF_IN_GGAGAA(X, Y, A, Z, B, W)
IF_IN_GGAGAA(X, Y, A, Z, B, W) → CALL1_IN_GGAGA(X, Y, A, Z, B)
CALL1_IN_GGAGA(X, Y, A, Z, B) → U13_GGAGA(X, Y, A, Z, B, count_in_gga(X, Y, A))
U13_GGAGA(X, Y, A, Z, B, count_out_gga(X, Y, A)) → OCCUR_IN_GGA(X, Z, B)
The TRS R consists of the following rules:
count_in_gga(X, [], 0) → count_out_gga(X, [], 0)
count_in_gga(X, .(Y, Z), W) → U2_gga(X, Y, Z, W, if1_in_ggaga(X, Z, W1, Y, W))
U2_gga(X, Y, Z, W, if1_out_ggaga(X, Z, W1, Y, W)) → count_out_gga(X, .(Y, Z), W)
if1_in_ggaga(X, Z, W1, Y, W) → U11_ggaga(X, Z, W1, Y, W, call2_in_gga(X, Z, W1))
U11_ggaga(X, Z, W1, Y, W, call2_out_gga(X, Z, W1)) → U12_ggaga(X, Z, W1, Y, W, addx_in_ggaa(X, Y, W1, W))
call2_in_gga(X, Z, W1) → U15_gga(X, Z, W1, count_in_gga(X, Z, W1))
U12_ggaga(X, Z, W1, Y, W, addx_out_ggaa(X, Y, W1, W)) → if1_out_ggaga(X, Z, W1, Y, W)
U15_gga(X, Z, W1, count_out_gga(X, Z, W1)) → call2_out_gga(X, Z, W1)
addx_in_ggaa(X, X, W1, W) → U3_ggaa(X, W1, W, is_in_aa(W, +(W1, 1)))
addx_in_ggaa(X, Y, W1, W1) → U4_ggaa(X, Y, W1, =\=_in_gg(X, Y))
U3_ggaa(X, W1, W, is_out_aa(W, +(W1, 1))) → addx_out_ggaa(X, X, W1, W)
U4_ggaa(X, Y, W1, =\=_out_gg(X, Y)) → addx_out_ggaa(X, Y, W1, W1)
is_in_aa(X0, X1) → is_out_aa(X0, X1)
=\=_in_gg(X0, X1) → =\=_out_gg(X0, X1)
The argument filtering Pi contains the following mapping:
[] =
[]
.(
x1,
x2) =
.(
x1,
x2)
count_in_gga(
x1,
x2,
x3) =
count_in_gga(
x1,
x2)
count_out_gga(
x1,
x2,
x3) =
count_out_gga
U2_gga(
x1,
x2,
x3,
x4,
x5) =
U2_gga(
x5)
if1_in_ggaga(
x1,
x2,
x3,
x4,
x5) =
if1_in_ggaga(
x1,
x2,
x4)
U11_ggaga(
x1,
x2,
x3,
x4,
x5,
x6) =
U11_ggaga(
x1,
x4,
x6)
call2_in_gga(
x1,
x2,
x3) =
call2_in_gga(
x1,
x2)
U15_gga(
x1,
x2,
x3,
x4) =
U15_gga(
x4)
call2_out_gga(
x1,
x2,
x3) =
call2_out_gga
U12_ggaga(
x1,
x2,
x3,
x4,
x5,
x6) =
U12_ggaga(
x6)
+(
x1,
x2) =
+(
x1,
x2)
1 =
1
=\=_in_gg(
x1,
x2) =
=\=_in_gg(
x1,
x2)
=\=_out_gg(
x1,
x2) =
=\=_out_gg
if1_out_ggaga(
x1,
x2,
x3,
x4,
x5) =
if1_out_ggaga
addx_in_ggaa(
x1,
x2,
x3,
x4) =
addx_in_ggaa(
x1,
x2)
U3_ggaa(
x1,
x2,
x3,
x4) =
U3_ggaa(
x4)
is_in_aa(
x1,
x2) =
is_in_aa
is_out_aa(
x1,
x2) =
is_out_aa
addx_out_ggaa(
x1,
x2,
x3,
x4) =
addx_out_ggaa
U4_ggaa(
x1,
x2,
x3,
x4) =
U4_ggaa(
x4)
OCCUR_IN_GGA(
x1,
x2,
x3) =
OCCUR_IN_GGA(
x1,
x2)
IF_IN_GGAGAA(
x1,
x2,
x3,
x4,
x5,
x6) =
IF_IN_GGAGAA(
x1,
x2,
x4)
CALL1_IN_GGAGA(
x1,
x2,
x3,
x4,
x5) =
CALL1_IN_GGAGA(
x1,
x2,
x4)
U13_GGAGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U13_GGAGA(
x1,
x4,
x6)
We have to consider all (P,R,Pi)-chains
(27) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(28) Obligation:
Q DP problem:
The TRS P consists of the following rules:
OCCUR_IN_GGA(X, .(Y, Z)) → IF_IN_GGAGAA(X, Y, Z)
IF_IN_GGAGAA(X, Y, Z) → CALL1_IN_GGAGA(X, Y, Z)
CALL1_IN_GGAGA(X, Y, Z) → U13_GGAGA(X, Z, count_in_gga(X, Y))
U13_GGAGA(X, Z, count_out_gga) → OCCUR_IN_GGA(X, Z)
The TRS R consists of the following rules:
count_in_gga(X, []) → count_out_gga
count_in_gga(X, .(Y, Z)) → U2_gga(if1_in_ggaga(X, Z, Y))
U2_gga(if1_out_ggaga) → count_out_gga
if1_in_ggaga(X, Z, Y) → U11_ggaga(X, Y, call2_in_gga(X, Z))
U11_ggaga(X, Y, call2_out_gga) → U12_ggaga(addx_in_ggaa(X, Y))
call2_in_gga(X, Z) → U15_gga(count_in_gga(X, Z))
U12_ggaga(addx_out_ggaa) → if1_out_ggaga
U15_gga(count_out_gga) → call2_out_gga
addx_in_ggaa(X, X) → U3_ggaa(is_in_aa)
addx_in_ggaa(X, Y) → U4_ggaa(=\=_in_gg(X, Y))
U3_ggaa(is_out_aa) → addx_out_ggaa
U4_ggaa(=\=_out_gg) → addx_out_ggaa
is_in_aa → is_out_aa
=\=_in_gg(X0, X1) → =\=_out_gg
The set Q consists of the following terms:
count_in_gga(x0, x1)
U2_gga(x0)
if1_in_ggaga(x0, x1, x2)
U11_ggaga(x0, x1, x2)
call2_in_gga(x0, x1)
U12_ggaga(x0)
U15_gga(x0)
addx_in_ggaa(x0, x1)
U3_ggaa(x0)
U4_ggaa(x0)
is_in_aa
=\=_in_gg(x0, x1)
We have to consider all (P,Q,R)-chains.
(29) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- IF_IN_GGAGAA(X, Y, Z) → CALL1_IN_GGAGA(X, Y, Z)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3
- U13_GGAGA(X, Z, count_out_gga) → OCCUR_IN_GGA(X, Z)
The graph contains the following edges 1 >= 1, 2 >= 2
- CALL1_IN_GGAGA(X, Y, Z) → U13_GGAGA(X, Z, count_in_gga(X, Y))
The graph contains the following edges 1 >= 1, 3 >= 2
- OCCUR_IN_GGA(X, .(Y, Z)) → IF_IN_GGAGAA(X, Y, Z)
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3
(30) YES
(31) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
U5_GGA(X, Y, Z, W, V, occur_out_gga(X, Z, W)) → OCCURALL_IN_GGA(Y, Z, V)
OCCURALL_IN_GGA(.(X, Y), Z, .(.(X, .(W, [])), V)) → U5_GGA(X, Y, Z, W, V, occur_in_gga(X, Z, W))
The TRS R consists of the following rules:
occurall_in_gga([], X, []) → occurall_out_gga([], X, [])
occurall_in_gga(.(X, Y), Z, .(.(X, .(W, [])), V)) → U5_gga(X, Y, Z, W, V, occur_in_gga(X, Z, W))
occur_in_gga(X, [], 0) → occur_out_gga(X, [], 0)
occur_in_gga(X, .(Y, Z), W) → U1_gga(X, Y, Z, W, if_in_ggagaa(X, Y, A, Z, B, W))
if_in_ggagaa(X, Y, A, Z, B, W) → U9_ggagaa(X, Y, A, Z, B, W, call1_in_ggaga(X, Y, A, Z, B))
call1_in_ggaga(X, Y, A, Z, B) → U13_ggaga(X, Y, A, Z, B, count_in_gga(X, Y, A))
count_in_gga(X, [], 0) → count_out_gga(X, [], 0)
count_in_gga(X, .(Y, Z), W) → U2_gga(X, Y, Z, W, if1_in_ggaga(X, Z, W1, Y, W))
if1_in_ggaga(X, Z, W1, Y, W) → U11_ggaga(X, Z, W1, Y, W, call2_in_gga(X, Z, W1))
call2_in_gga(X, Z, W1) → U15_gga(X, Z, W1, count_in_gga(X, Z, W1))
U15_gga(X, Z, W1, count_out_gga(X, Z, W1)) → call2_out_gga(X, Z, W1)
U11_ggaga(X, Z, W1, Y, W, call2_out_gga(X, Z, W1)) → U12_ggaga(X, Z, W1, Y, W, addx_in_ggaa(X, Y, W1, W))
addx_in_ggaa(X, X, W1, W) → U3_ggaa(X, W1, W, is_in_aa(W, +(W1, 1)))
is_in_aa(X0, X1) → is_out_aa(X0, X1)
U3_ggaa(X, W1, W, is_out_aa(W, +(W1, 1))) → addx_out_ggaa(X, X, W1, W)
addx_in_ggaa(X, Y, W1, W1) → U4_ggaa(X, Y, W1, =\=_in_gg(X, Y))
=\=_in_gg(X0, X1) → =\=_out_gg(X0, X1)
U4_ggaa(X, Y, W1, =\=_out_gg(X, Y)) → addx_out_ggaa(X, Y, W1, W1)
U12_ggaga(X, Z, W1, Y, W, addx_out_ggaa(X, Y, W1, W)) → if1_out_ggaga(X, Z, W1, Y, W)
U2_gga(X, Y, Z, W, if1_out_ggaga(X, Z, W1, Y, W)) → count_out_gga(X, .(Y, Z), W)
U13_ggaga(X, Y, A, Z, B, count_out_gga(X, Y, A)) → U14_ggaga(X, Y, A, Z, B, occur_in_gga(X, Z, B))
U14_ggaga(X, Y, A, Z, B, occur_out_gga(X, Z, B)) → call1_out_ggaga(X, Y, A, Z, B)
U9_ggagaa(X, Y, A, Z, B, W, call1_out_ggaga(X, Y, A, Z, B)) → U10_ggagaa(X, Y, A, Z, B, W, is_in_aa(W, +(A, B)))
U10_ggagaa(X, Y, A, Z, B, W, is_out_aa(W, +(A, B))) → if_out_ggagaa(X, Y, A, Z, B, W)
U1_gga(X, Y, Z, W, if_out_ggagaa(X, Y, A, Z, B, W)) → occur_out_gga(X, .(Y, Z), W)
U5_gga(X, Y, Z, W, V, occur_out_gga(X, Z, W)) → U6_gga(X, Y, Z, W, V, occurall_in_gga(Y, Z, V))
U6_gga(X, Y, Z, W, V, occurall_out_gga(Y, Z, V)) → occurall_out_gga(.(X, Y), Z, .(.(X, .(W, [])), V))
The argument filtering Pi contains the following mapping:
occurall_in_gga(
x1,
x2,
x3) =
occurall_in_gga(
x1,
x2)
[] =
[]
occurall_out_gga(
x1,
x2,
x3) =
occurall_out_gga
.(
x1,
x2) =
.(
x1,
x2)
U5_gga(
x1,
x2,
x3,
x4,
x5,
x6) =
U5_gga(
x2,
x3,
x6)
occur_in_gga(
x1,
x2,
x3) =
occur_in_gga(
x1,
x2)
occur_out_gga(
x1,
x2,
x3) =
occur_out_gga
U1_gga(
x1,
x2,
x3,
x4,
x5) =
U1_gga(
x5)
if_in_ggagaa(
x1,
x2,
x3,
x4,
x5,
x6) =
if_in_ggagaa(
x1,
x2,
x4)
U9_ggagaa(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U9_ggagaa(
x7)
call1_in_ggaga(
x1,
x2,
x3,
x4,
x5) =
call1_in_ggaga(
x1,
x2,
x4)
U13_ggaga(
x1,
x2,
x3,
x4,
x5,
x6) =
U13_ggaga(
x1,
x4,
x6)
count_in_gga(
x1,
x2,
x3) =
count_in_gga(
x1,
x2)
count_out_gga(
x1,
x2,
x3) =
count_out_gga
U2_gga(
x1,
x2,
x3,
x4,
x5) =
U2_gga(
x5)
if1_in_ggaga(
x1,
x2,
x3,
x4,
x5) =
if1_in_ggaga(
x1,
x2,
x4)
U11_ggaga(
x1,
x2,
x3,
x4,
x5,
x6) =
U11_ggaga(
x1,
x4,
x6)
call2_in_gga(
x1,
x2,
x3) =
call2_in_gga(
x1,
x2)
U15_gga(
x1,
x2,
x3,
x4) =
U15_gga(
x4)
call2_out_gga(
x1,
x2,
x3) =
call2_out_gga
U12_ggaga(
x1,
x2,
x3,
x4,
x5,
x6) =
U12_ggaga(
x6)
+(
x1,
x2) =
+(
x1,
x2)
1 =
1
=\=_in_gg(
x1,
x2) =
=\=_in_gg(
x1,
x2)
=\=_out_gg(
x1,
x2) =
=\=_out_gg
if1_out_ggaga(
x1,
x2,
x3,
x4,
x5) =
if1_out_ggaga
addx_in_ggaa(
x1,
x2,
x3,
x4) =
addx_in_ggaa(
x1,
x2)
U3_ggaa(
x1,
x2,
x3,
x4) =
U3_ggaa(
x4)
is_in_aa(
x1,
x2) =
is_in_aa
is_out_aa(
x1,
x2) =
is_out_aa
addx_out_ggaa(
x1,
x2,
x3,
x4) =
addx_out_ggaa
U4_ggaa(
x1,
x2,
x3,
x4) =
U4_ggaa(
x4)
U14_ggaga(
x1,
x2,
x3,
x4,
x5,
x6) =
U14_ggaga(
x6)
call1_out_ggaga(
x1,
x2,
x3,
x4,
x5) =
call1_out_ggaga
U10_ggagaa(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U10_ggagaa(
x7)
if_out_ggagaa(
x1,
x2,
x3,
x4,
x5,
x6) =
if_out_ggagaa
U6_gga(
x1,
x2,
x3,
x4,
x5,
x6) =
U6_gga(
x6)
OCCURALL_IN_GGA(
x1,
x2,
x3) =
OCCURALL_IN_GGA(
x1,
x2)
U5_GGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U5_GGA(
x2,
x3,
x6)
We have to consider all (P,R,Pi)-chains
(32) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(33) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
U5_GGA(X, Y, Z, W, V, occur_out_gga(X, Z, W)) → OCCURALL_IN_GGA(Y, Z, V)
OCCURALL_IN_GGA(.(X, Y), Z, .(.(X, .(W, [])), V)) → U5_GGA(X, Y, Z, W, V, occur_in_gga(X, Z, W))
The TRS R consists of the following rules:
occur_in_gga(X, [], 0) → occur_out_gga(X, [], 0)
occur_in_gga(X, .(Y, Z), W) → U1_gga(X, Y, Z, W, if_in_ggagaa(X, Y, A, Z, B, W))
U1_gga(X, Y, Z, W, if_out_ggagaa(X, Y, A, Z, B, W)) → occur_out_gga(X, .(Y, Z), W)
if_in_ggagaa(X, Y, A, Z, B, W) → U9_ggagaa(X, Y, A, Z, B, W, call1_in_ggaga(X, Y, A, Z, B))
U9_ggagaa(X, Y, A, Z, B, W, call1_out_ggaga(X, Y, A, Z, B)) → U10_ggagaa(X, Y, A, Z, B, W, is_in_aa(W, +(A, B)))
call1_in_ggaga(X, Y, A, Z, B) → U13_ggaga(X, Y, A, Z, B, count_in_gga(X, Y, A))
U10_ggagaa(X, Y, A, Z, B, W, is_out_aa(W, +(A, B))) → if_out_ggagaa(X, Y, A, Z, B, W)
U13_ggaga(X, Y, A, Z, B, count_out_gga(X, Y, A)) → U14_ggaga(X, Y, A, Z, B, occur_in_gga(X, Z, B))
is_in_aa(X0, X1) → is_out_aa(X0, X1)
count_in_gga(X, [], 0) → count_out_gga(X, [], 0)
count_in_gga(X, .(Y, Z), W) → U2_gga(X, Y, Z, W, if1_in_ggaga(X, Z, W1, Y, W))
U14_ggaga(X, Y, A, Z, B, occur_out_gga(X, Z, B)) → call1_out_ggaga(X, Y, A, Z, B)
U2_gga(X, Y, Z, W, if1_out_ggaga(X, Z, W1, Y, W)) → count_out_gga(X, .(Y, Z), W)
if1_in_ggaga(X, Z, W1, Y, W) → U11_ggaga(X, Z, W1, Y, W, call2_in_gga(X, Z, W1))
U11_ggaga(X, Z, W1, Y, W, call2_out_gga(X, Z, W1)) → U12_ggaga(X, Z, W1, Y, W, addx_in_ggaa(X, Y, W1, W))
call2_in_gga(X, Z, W1) → U15_gga(X, Z, W1, count_in_gga(X, Z, W1))
U12_ggaga(X, Z, W1, Y, W, addx_out_ggaa(X, Y, W1, W)) → if1_out_ggaga(X, Z, W1, Y, W)
U15_gga(X, Z, W1, count_out_gga(X, Z, W1)) → call2_out_gga(X, Z, W1)
addx_in_ggaa(X, X, W1, W) → U3_ggaa(X, W1, W, is_in_aa(W, +(W1, 1)))
addx_in_ggaa(X, Y, W1, W1) → U4_ggaa(X, Y, W1, =\=_in_gg(X, Y))
U3_ggaa(X, W1, W, is_out_aa(W, +(W1, 1))) → addx_out_ggaa(X, X, W1, W)
U4_ggaa(X, Y, W1, =\=_out_gg(X, Y)) → addx_out_ggaa(X, Y, W1, W1)
=\=_in_gg(X0, X1) → =\=_out_gg(X0, X1)
The argument filtering Pi contains the following mapping:
[] =
[]
.(
x1,
x2) =
.(
x1,
x2)
occur_in_gga(
x1,
x2,
x3) =
occur_in_gga(
x1,
x2)
occur_out_gga(
x1,
x2,
x3) =
occur_out_gga
U1_gga(
x1,
x2,
x3,
x4,
x5) =
U1_gga(
x5)
if_in_ggagaa(
x1,
x2,
x3,
x4,
x5,
x6) =
if_in_ggagaa(
x1,
x2,
x4)
U9_ggagaa(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U9_ggagaa(
x7)
call1_in_ggaga(
x1,
x2,
x3,
x4,
x5) =
call1_in_ggaga(
x1,
x2,
x4)
U13_ggaga(
x1,
x2,
x3,
x4,
x5,
x6) =
U13_ggaga(
x1,
x4,
x6)
count_in_gga(
x1,
x2,
x3) =
count_in_gga(
x1,
x2)
count_out_gga(
x1,
x2,
x3) =
count_out_gga
U2_gga(
x1,
x2,
x3,
x4,
x5) =
U2_gga(
x5)
if1_in_ggaga(
x1,
x2,
x3,
x4,
x5) =
if1_in_ggaga(
x1,
x2,
x4)
U11_ggaga(
x1,
x2,
x3,
x4,
x5,
x6) =
U11_ggaga(
x1,
x4,
x6)
call2_in_gga(
x1,
x2,
x3) =
call2_in_gga(
x1,
x2)
U15_gga(
x1,
x2,
x3,
x4) =
U15_gga(
x4)
call2_out_gga(
x1,
x2,
x3) =
call2_out_gga
U12_ggaga(
x1,
x2,
x3,
x4,
x5,
x6) =
U12_ggaga(
x6)
+(
x1,
x2) =
+(
x1,
x2)
1 =
1
=\=_in_gg(
x1,
x2) =
=\=_in_gg(
x1,
x2)
=\=_out_gg(
x1,
x2) =
=\=_out_gg
if1_out_ggaga(
x1,
x2,
x3,
x4,
x5) =
if1_out_ggaga
addx_in_ggaa(
x1,
x2,
x3,
x4) =
addx_in_ggaa(
x1,
x2)
U3_ggaa(
x1,
x2,
x3,
x4) =
U3_ggaa(
x4)
is_in_aa(
x1,
x2) =
is_in_aa
is_out_aa(
x1,
x2) =
is_out_aa
addx_out_ggaa(
x1,
x2,
x3,
x4) =
addx_out_ggaa
U4_ggaa(
x1,
x2,
x3,
x4) =
U4_ggaa(
x4)
U14_ggaga(
x1,
x2,
x3,
x4,
x5,
x6) =
U14_ggaga(
x6)
call1_out_ggaga(
x1,
x2,
x3,
x4,
x5) =
call1_out_ggaga
U10_ggagaa(
x1,
x2,
x3,
x4,
x5,
x6,
x7) =
U10_ggagaa(
x7)
if_out_ggagaa(
x1,
x2,
x3,
x4,
x5,
x6) =
if_out_ggagaa
OCCURALL_IN_GGA(
x1,
x2,
x3) =
OCCURALL_IN_GGA(
x1,
x2)
U5_GGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U5_GGA(
x2,
x3,
x6)
We have to consider all (P,R,Pi)-chains
(34) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(35) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U5_GGA(Y, Z, occur_out_gga) → OCCURALL_IN_GGA(Y, Z)
OCCURALL_IN_GGA(.(X, Y), Z) → U5_GGA(Y, Z, occur_in_gga(X, Z))
The TRS R consists of the following rules:
occur_in_gga(X, []) → occur_out_gga
occur_in_gga(X, .(Y, Z)) → U1_gga(if_in_ggagaa(X, Y, Z))
U1_gga(if_out_ggagaa) → occur_out_gga
if_in_ggagaa(X, Y, Z) → U9_ggagaa(call1_in_ggaga(X, Y, Z))
U9_ggagaa(call1_out_ggaga) → U10_ggagaa(is_in_aa)
call1_in_ggaga(X, Y, Z) → U13_ggaga(X, Z, count_in_gga(X, Y))
U10_ggagaa(is_out_aa) → if_out_ggagaa
U13_ggaga(X, Z, count_out_gga) → U14_ggaga(occur_in_gga(X, Z))
is_in_aa → is_out_aa
count_in_gga(X, []) → count_out_gga
count_in_gga(X, .(Y, Z)) → U2_gga(if1_in_ggaga(X, Z, Y))
U14_ggaga(occur_out_gga) → call1_out_ggaga
U2_gga(if1_out_ggaga) → count_out_gga
if1_in_ggaga(X, Z, Y) → U11_ggaga(X, Y, call2_in_gga(X, Z))
U11_ggaga(X, Y, call2_out_gga) → U12_ggaga(addx_in_ggaa(X, Y))
call2_in_gga(X, Z) → U15_gga(count_in_gga(X, Z))
U12_ggaga(addx_out_ggaa) → if1_out_ggaga
U15_gga(count_out_gga) → call2_out_gga
addx_in_ggaa(X, X) → U3_ggaa(is_in_aa)
addx_in_ggaa(X, Y) → U4_ggaa(=\=_in_gg(X, Y))
U3_ggaa(is_out_aa) → addx_out_ggaa
U4_ggaa(=\=_out_gg) → addx_out_ggaa
=\=_in_gg(X0, X1) → =\=_out_gg
The set Q consists of the following terms:
occur_in_gga(x0, x1)
U1_gga(x0)
if_in_ggagaa(x0, x1, x2)
U9_ggagaa(x0)
call1_in_ggaga(x0, x1, x2)
U10_ggagaa(x0)
U13_ggaga(x0, x1, x2)
is_in_aa
count_in_gga(x0, x1)
U14_ggaga(x0)
U2_gga(x0)
if1_in_ggaga(x0, x1, x2)
U11_ggaga(x0, x1, x2)
call2_in_gga(x0, x1)
U12_ggaga(x0)
U15_gga(x0)
addx_in_ggaa(x0, x1)
U3_ggaa(x0)
U4_ggaa(x0)
=\=_in_gg(x0, x1)
We have to consider all (P,Q,R)-chains.
(36) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- OCCURALL_IN_GGA(.(X, Y), Z) → U5_GGA(Y, Z, occur_in_gga(X, Z))
The graph contains the following edges 1 > 1, 2 >= 2
- U5_GGA(Y, Z, occur_out_gga) → OCCURALL_IN_GGA(Y, Z)
The graph contains the following edges 1 >= 1, 2 >= 2
(37) YES